4

One way to solve optimisation problems is to use an SMT solver to ask whether a (bad) solution exists, then to progressively add tighter cost constraints until the proposition is no longer satisfiable. This approach is discussed in, for example, http://www.lsi.upc.edu/~oliveras/espai/papers/sat06.pdf and http://isi.uni-bremen.de/agra/doc/konf/08_isvlsi_optprob.pdf.

Is this approach efficient, though? i.e. will the solver re-use information from previous solutions when attempting to solve with additional constraints?

Tom Perry
  • 55
  • 3

1 Answers1

6

The solver can reuse lemmas learned when trying to solve previous queries. Just keep in mind than in Z3 whenever you execute a pop all lemmas (created since the corresponding push) are forgotten. So, to accomplish that you must avoid push and pop commands and use "assumptions" if you need to retract assertions. In the following question, I describe how to use "assumptions" in Z3: Soft/Hard constraints in Z3

Regarding efficiency, this approach is not the most efficient one for every problem domain. On the other hand, it can be implemented on top of most SMT solvers. Moreover, Pseudo-Boolean solvers (solver for 0-1 integer problems) successfully use a similar approach for solving optimization problems.

Community
  • 1
  • 1
Leonardo de Moura
  • 21,065
  • 2
  • 47
  • 53
  • 1
    Is there a way to save the lemmas from Z3 and add the lemmas to Z3 for solving later? – user Dec 08 '14 at 01:31