Skip to main content

Convex quadratic optimisation modulo linear arithmetic

Supervisor

Suitable for

Mathematics and Computer Science, Part C
Computer Science and Philosophy, Part C
Computer Science, Part C

Abstract

Optimisation modulo theories is a new paradigm in which one optimises an objective function subject to a Boolean combination of linear constraints. The open-source SMT-solver Z3 currently only supports optimising linear objective functions. The goal of this project is to add support for optimising convex quadratic functions to Z3 based on the classical Frank-Wolfe algorithm.