Simplex in z3 via for-all

Question

A very similar questions were asked on SO already, but I couldn't find answer to the following problem. A linear maximization problem can be easily stated using for-all quantifier:

obj = f(x) AND \forall x . Ax <= b => f(x) <= obj

The queries like above can be posed to z3. Consequently I want to ask whether z3 is smart enough to recognize an LP problem when it sees one and will it apply a simplex method to eliminate a for-all quantifier?

I did a few experiments and it seemed to work, but I haven't tried it on more complex examples.

Thanks!

Fusspot

Answer 1

Z3 does not recognize it as an LP optimization problem. It most likely applies quantifier elimination first on the universally quantified formula, then the result is quantifier-free linear arithmetic and the model that comes out will provide the maximal value for the objective. This is of course not an efficient way to solve optimization problems. If you have courage to experiment, then the branch called "opt" under z3.codeplex.com contains an extension to Z3 that lets you formulate optimization objectives with Z3. A description of how to use it will be available soon.

Buroker

thank you! Is the code in the opt branch the one referenced in the paper "Symbolic Optimization with SMT Solvers" (implemented by Arie and others if I recall correctly) – Fusspot

EDIT: I was referring to z3.codeplex.com/SourceControl/network/forks/arie/…, I presume opt- does something else? – Fusspot