CODEWITHSUNDEEP
optimizationz3smt
buggymcbugfix
buggymcbugfix

Reputation: 321

Best-effort (max|min)imisation in Z3 optimisations

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?

Upvotes: 1

Views: 104

Answers (1)

alias
alias

Reputation: 30418

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

Upvotes: 2

Related Questions