How to check progress for Z3 optimization problem

Question

I have a problem which I code up in an smt-lib file for input into Z3. There are many constraints, but really, I am interested in minimizing one variable:

        (minimize totalCost)
        (check-sat)

The solver runs, and runs, for hours. Much longer than if I were to simply use an assert to set totalCost below some value and run check-sat. Is there any way to get Z3 to periodically print out the lowest value it has achieved for totalCost, along with all the variable values to achieve that? That would be very helpful. Thanks in advance!

Answer 1

Looking at the verbose mode as Patrick described is your best bet if you want to stick to the optimizing solver. Of course, the output might be hard to understand and may not even have all the data you need. You can "instrument" z3 source code to print out more if you dig deep into it. But that's a lot more work and would need studying the source code.

But it occurs to me that z3 is doing quite well with your constraints, it's the optimization engine that slows down? That's not surprising, as the optimizing solver is not as performant as the regular solver for obvious reasons. If you suspect this is the case, you might want to optimize by doing an outer loop: Do a check-sat, get the value of totalCost, then ask again but add the extra constraint that totalCost is less than the current value provided. This can quickly converge for certain problems: If the solution space is small enough and you use many different theories, this technique can outperform the optimizing solver. You can also implement a "binary" search of sorts: For instance, if the solver gives you a solution with cost 100, you can ask if there's one with cost less than 50; if sat, you'd then ask for 25, if unsat, you'd ask for 75. Depending on your problem, this can be very effective.

Note that if you implement the above trick, you can also use the solver in the incremental mode, and it would re-use all the lemmas it learned from before. The optimizing solver itself is not incremental, so that's another advantage of the looping technique. On the other hand, if there are too many solutions to your constraints, or if you don't have a global minimum, then the looping technique can run forever: So you probably want to watch for the loop-count and stop after a certain threshold.

Answer 2

If you run z3 via the command-line, you may try the option -v:1, which makes the OMT solver print any update to the lower/upper bounds of the cost function.

e.g.

~$ z3 -v:1 optimathsat/tools/release_files/examples/optimization/smtlib2_binary.smt2
...
(optsmt upper bound: 57)
(optsmt upper bound: 54)
(optsmt upper bound: 157/3)
(optsmt upper bound: 52)
(optsmt upper bound: 154/3)
(optsmt upper bound: 50)
(optsmt upper bound: 149/3)
(optsmt upper bound: 97/2)
(optsmt upper bound: 145/3)
(optsmt upper bound: 48)
(optsmt upper bound: 95/2)
(optsmt upper bound: 140/3)
(optsmt upper bound: 46)
(optsmt upper bound: 181/4)
(optsmt upper bound: 45)
(optsmt upper bound: 134/3)
(optsmt upper bound: 89/2)
(optsmt upper bound: 177/4)
(optsmt upper bound: 44)
(optsmt upper bound: 43)
(optsmt upper bound: 171/4)
(optsmt upper bound: 128/3)
(optsmt upper bound: 85/2)
(optsmt upper bound: 42)
(optsmt upper bound: 81/2)
(optsmt upper bound: 202/5)
(optsmt upper bound: 40)
(optsmt upper bound: 199/5)
(optsmt upper bound: 193/5)
(optsmt upper bound: 77/2)
(optsmt upper bound: 192/5)
(optsmt upper bound: 115/3)
(optsmt upper bound: 191/5)
(optsmt upper bound: 189/5)
(optsmt upper bound: 217/6)
(optsmt upper bound: 36)
(optsmt upper bound: 69/2)
(optsmt upper bound: 137/4)
(optsmt upper bound: 34)
(optsmt upper bound: 65/2)
(optsmt upper bound: 223/7)
(optsmt upper bound: 63/2)
(optsmt upper bound: 218/7)
(optsmt upper bound: 216/7)
(optsmt upper bound: 123/4)
(optsmt upper bound: 61/2)
(optsmt upper bound: 211/7)
(optsmt upper bound: 241/8)
(optsmt upper bound: 30)
(optsmt upper bound: 208/7)
(optsmt upper bound: 59/2)
(optsmt upper bound: 115/4)
(optsmt upper bound: 57/2)
(optsmt upper bound: 113/4)
(optsmt upper bound: 253/9)
(optsmt upper bound: 251/9)
(optsmt upper bound: 250/9)
(optsmt upper bound: 221/8)
(optsmt upper bound: 55/2)
(optsmt upper bound: 192/7)
(optsmt upper bound: 191/7)
(optsmt upper bound: 109/4)
(optsmt upper bound: 217/8)
(optsmt upper bound: 27)
sat
(objectives
 (objective 27)
)

This is only useful when the optimization algorithm being used advances the search starting from the satisfiable region. Some optimization engines like, e.g. MaxRes, approach the optimal solution starting from the unsatisfiable (i.e. more-than-optimal) region, and therefore do not provide any partial solution (however, they may be considerably faster on some instances).