Z3 getting last valid model

0
votes

I using Z3 C++ api to find a satisfiable formula that is minimal with respect to some boolean variables (let us call them b0,...,bn) being true.

I have a formula that includes boolean variables b0,...,bn and I want to find some satisfiable formula where I have the least number of b0,...,bn set to true.

I do this by initially finding a subset of b0,...,bn that can be assigned to true and satisfy my formula, and I incrementally ask the solver to find smaller subsets (i.e. where one of these boolean variables is flipped to false).

I find my local minimum when I cannot find a smaller subset, i.e. I get a unsat result from the Z3. At this point, I would like to access the last valid model.

Is that possible? Does Z3 modify the model when a call to "check" is unsat? If so, how can I do this using the C++ api?

Many thanks in advance,

2
z3

2 Answers

0
votes

You can retrieve a model if the solver returns "sat". The model refers to the state of the solver, so if you add assertions, the state changes and models are no longer valid until you check satisfiability and it returns sat. So you can retrieve a model every time the solver returns SAT, and then discharge all but the last model.

0
votes

As Nikolaj mentioned, you need to keep track of models after each call that results in sat and return the last one when you get an unsat if you follow the strategy you outlined.

However, there might be another alternative that avoids repeated calls altogether. Instead of a satisfaction problem, you can cast your problem as an optimization one. You mentioned you have control variables b0, b1, .. bn such that you want to minimize the number of them getting set to true for a satisfying model. Create a metric that counts the number of ones in these variables. Something like:

metric = (if b0 then 1 else 0)
       + (if b1 then 1 else 0)
       + ...
       + (if bn then 1 else 0)

Then use Z3's optimization routines to minimize metric. I believe this will provide you with the solution you are looking for in one call only.

Some helpful references: