I'm new to Z3, and trying to make a solver which returns every satisfiable solution to a boolean formula. Taking notes from other SO-posts, I've coded what I hoped would work, but isn't. The problem seems to that by adding the previous solutions, I remove some of the variables, but then they return in later solutions?
Currently I am just trying to solve a or b or c.
If I explained poorly, let me know and I will try to explain further.
Thanks in advance for the response :)
My code:
from z3 import *
a, b, c = Bools('a b c')
s = Solver()
s.add(Or([a, b, c]))
while (s.check() == sat):
print(s.check())
print(s)
print(s.model())
print(s.model().decls())
print("\n")
s.add(Or([ f() != s.model()[f] for f in s.model().decls() if f.arity() == 0]))
My output:
sat
[Or(a, b, c)]
[c = False, b = False, a = True]
[c, b, a]
sat
[Or(a, b, c), Or(c != False, b != False, a != True)]
[b = True, a = False]
[b, a]
sat
[Or(a, b, c),
Or(c != False, b != False, a != True),
Or(b != True, a != False)]
[b = True, a = True]
[b, a]
sat
[Or(a, b, c),
Or(c != False, b != False, a != True),
Or(b != True, a != False),
Or(b != True, a != True)]
[b = False, c = True]
[b, c]
The typical way to code such problems is as follows:
This prints:
You'll notice that not all models are "complete." This is because z3 will typically "stop" assigning variables once it decides the problem is sat, as the other variables are irrelevant.
I suppose your confusion is that there should be 7 models to your problem: Aside from the all-False assignment, you should have a model. If you want to get the values of all your variables in this way, then you should explicitly query for them, like this:
This prints:
And there are exactly 7 models as you would've expected.
Note the
model_completion
parameter. This is a common pitfall for newcomers as there isn't a "out-of-the-box" method in z3 for getting all possible assignments, so you have to be careful coding it yourself like above. The reason why there isn't such a function is that it's really hard to implement it in general: Think about how it should work if your variables were functions, arrays, user-defined data-types, etc. as opposed to simple booleans. It can get really tricky to implement a generic all-sat function with all these possibilities handled correctly and efficiently. So, it's left to the user, as most of the time you only care about a specific notion of all-sat that's typically not hard to code once you learn the basic idioms.