1

I am interested in Z3 giving me a model and at the same time I would be happy if it tried to take an objective function into account as a heuristic, but I don't want to pay the performance penalty of finding the actual (max|min)imum.

Is this possible in Z3?

buggymcbugfix
  • 321
  • 1
  • 11

1 Answers1

2

This is already possible in Z3 with soft time outs, see this answer: Z3 Time Restricted Optimization

The way to achieve what you want is to use incremental solving:

  • Assert all your hard constraints. (i.e., those that need to be satisfied)
  • Do a check-sat and get the model
  • Assert all your "optimization" constraints.
  • Use a soft-time out, as described here: Z3 Time Restricted Optimization

In the last step, you can adjust how much you want to wait, i.e., the penalty you are willing to pay.

Related note: You might also want to play with soft-constraints, which the solver can "satisfy" optionally, incurring penalties if it doesn't. Perhaps that's more appropriate for your use case. See here on how to do that: https://rise4fun.com/Z3/tutorialcontent/optimization#h23

alias
  • 28,120
  • 2
  • 23
  • 40
  • 1
    Uuh, I stand corrected! I'll try this function too, thanks. How to set soft timeouts with smtlib syntax? I don't understand why you mention assert soft only, does it not work with standard objectives? – Patrick Trentin Mar 02 '18 at 15:28
  • 2
    @PatrickTrentin Quite right; I think it should work with regular constraints as well. See my edited answer. – alias Mar 02 '18 at 15:44