Z3: finding all satisfying models

问题:

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?

回答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]