Z3: finding all satisfying models

Question

I am trying to retrieve all possible models for some first-order theory using Z3, an SMT solver developed by Microsoft Research. Here is a minimal working example:

(declare-const f Bool)
(assert (or (= f true) (= f false)))

In this propositional case there are two satisfying assignments: f->true and f->false. Because Z3 (and SMT solvers in general) will only try to find one satisfying model, finding all solutions is not directly possible. Here I found a useful command called (next-sat), but it seems that the latest version of Z3 no longer supports this. This is bit unfortunate for me, and in general I think the command is quite useful. Is there another way of doing this?

Seadon

Answer 1

One way to accomplish this is using one of the APIs, along with the model generation capability. You can then use the generated model from one satisfiability check to add constraints to prevent previous model values from being used in subsequent satisfiability checks, until there are no more satisfying assignments. Of course, you have to be using finite sorts (or have some constraints ensuring this), but you could use this with infinite sorts as well if you don't want to find all possible models (i.e., stop after you generate a bunch).

Here is an example using z3py (link to z3py script: http://rise4fun.com/Z3Py/a6MC ):

a = Int('a')
b = Int('b')

s = Solver()
s.add(1 <= a)
s.add(a <= 20)
s.add(1 <= b)
s.add(b <= 20)
s.add(a >= 2*b)

while s.check() == sat:
  print s.model()
  s.add(Or(a != s.model()[a], b != s.model()[b])) # prevent next model from using the same assignment as a previous model

In general, using the disjunct of all the involved constants should work (e.g., a and b here). This enumerates all integer assignments for a and b (between 1 and 20) satisfying a >= 2b. For example, if we restrict a and b to lie between 1 and 5 instead, the output is:

[b = 1, a = 2]
[b = 2, a = 4]
[b = 1, a = 3]
[b = 2, a = 5]
[b = 1, a = 4]
[b = 1, a = 5]

Unswerving

Also, see this answer: #11868111 – Unswerving

Is Z3 stateful in the sense that it will pick up where it left off for such a search? It seems it would be wasteful to start over each time, when (intuitively) all the work is exactly the same except for the very end. – Maryn

@Maryn For the examples I've used this method with, it seems like it is indeed stateful in that finding the next few models after the initial one is faster. Here is a list of runtimes in milliseconds for a particular case with 58 models: 8942 801 1663 5 599 320 450 2 2 3 1 5 1377 36 5 738 162 105 1639 3 5 16 2041 27 475 953 562 746 45 151 18 4206 3416 9 850 120 3 4 12 615 593 1219 449 154 987 3 10 1365 16 438 792 1686 743 46 5 8 412 126. Notice that the first one is definitely the longest, but the others are more random (probably depends on the problem and how lucky the solver gets). – Assertive

@Maryn Yes, as long as you're using the same Solver object, it keeps all of its learned clauses. You can use push and pop to selectively forget learned clauses back to the last push (the only way to remove constraints is to pop back to a previous push). – Robomb

Answer 2

A more general solution based on Taylors answer would be to use

while s.check() == z3.sat:  
    solution = "False"
    m = s.model()
    for i in m:
        solution = f"Or(({i} != {m[i]}), {solution})"
    f2 = eval(solution)
    s.add(f2)

This allows more than two variables.

Westnorthwest

This solution can be quite inefficient, going back from strings/eval etc. Also, the way it blocks solutions isn't optimal. See https://mcmap.net/q/408711/-z3py-checking-all-solutions-for-equation for a much better approach. – Garrik