Optimization with quantified SMT solving

[rainoftime]

The standard optimization problem: min $f(x)$ s.t. $P(x)$ (P is a quantifier-free formula)
can be encoded as the logic formula: $P(x) \land \forall y . ( P(y) \to f(x) \leq f(y) )$

Therefore, it seems the opt module of z3 can provide an option for optimization with quantified SMT solving. For example, for bit-vector optimization problem, the ufbv tactic can be applied to solve the constructed quantified bit-vector formula.

Could you please give some advice on how to integrate such a mechanism into opt?

[NikolajBjorner]

Correct, but why integrate this with opt when this encoding works directly with solvers?
The encoding is not going to lead to an efficient procedure out of the box, even the algorithms for solving satisfiability of quantifiers, that have some abstraction-refinement flavor were so far not very convincing for solving optimization problems in this way (the idea extends to nested optimization objectives where you take a min of a max of a min etc).

[rainoftime]

Thank you for reply! Providing a uniform interface in opt might help take advantage of recent progress in quantified SMT solving.

• For QF_BV optimization, we may use the ufbv tactic
• For QF_LRA optmization, we may take qsat tactic that is based on abstraction refinement and "Model Based Projection".

Maybe I can collect some benchmarks for comparison.

[NikolajBjorner]

I tried integrating qsat for QF_LRA optimization. My results (on a single example) were poor in my view so it is disabled.
It should be driven by benchmarks. If you have benchmarks, it would be great.

[kgoyal40]

What is the best way to use quantifiers in with OMT?

[kgoyal40]

@rainoftime, Asking the question again in more detail. Do you have any suggestions on how to encode a quantified formula like the following to a non-quantified one (to be used with OMT)?:

W = RealVector('w', 5)
X = RealVector('x', 5)
ForAll(X, Implies(X[4] == 2, SumProduct(X, W) < 0)

**Here SumProduct is a user defined function

[NikolajBjorner]

A humble approach is: Pre-instantiate the quantifier with a suitable set of terms. Do ground optimization, then check if the result can be improved using quantified formula. An improvement provides additional instances.