1

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!

Helix888
  • 11
  • 2

2 Answers2

2

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.

alias
  • 28,120
  • 2
  • 23
  • 40
  • Thank you for the answers. The verbose option is helpful to see the progress. I wish there were a way to say 'run for 15 minutes, and either return 'undetermined' or the lowest cost it found, along with the necessary model/variable assignments.' I will try running in incremental mode as you suggested. Before, I was running with constraints like maxCost < 100 etc, but in individual sessions from scratch, it took a long time I was hoping minimize would be faster. – Helix888 Sep 18 '19 at 19:32
  • You can give z3 a time limit, but I don't think it dumps the "current" values when the time out expires. (Checkout the `-T` and `-t` options.) As Patrick mentioned, such a current value may not even be available depending on the constraints. Try the incremental mode with binary search; that might be your best bet. – alias Sep 18 '19 at 19:55
1

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).

Patrick Trentin
  • 7,126
  • 3
  • 23
  • 40