why z3 solver give bool variable "none", how to get rid of it?

Question

I am new to Z3py. I am trying to list all satisfied solutions to a bool formula (or to get the truth table which generate only True).

My code is here, inspired from another answer finding all satisfying models:

from z3 import *
A1, B1, B2, C1, C2, E1, E2, F4 = Bools('A1 B1 B2 C1 C2 E1 E2 F4')
s = Solver()
s.add(simplify(Or(And(A1, Or(C1, C2), Or(B1, B2), E2, F4), 
    And(A1, C2, Or(B1, B2), E1))))

while s.check() == sat:
  print(s.model())
  s.add(Or(A1 != s.model()[A1],
    B1 != s.model()[B1],
    B2 != s.model()[B2],
    C1 != s.model()[C1],
    C2 != s.model()[C2],
    E1 != s.model()[E1],
    E2 != s.model()[E2],
    F4 != s.model()[F4]))

but I got results like this:

True,True,None,None,True,True,False,None

True,True,None,None,True,True,False,None

True,True,None,None,True,True,False,None

True,True,None,None,True,True,False,None
...

as you can see, they have duplicated results, and there are "None" in it, why is this happening? Isn't it true that Bool variable has only "true" or "false"? Why there are duplicated models in it? Thank you very much.

score 1 · Answer 1 · answered Sep 02 '21 at 10:42

1

None is a don't-care; it means that you are free to choose either True or False and both are valid models. You can ask Z3 to fill in these values by enabling model completion, for example as it's done in How to model in Z3py

answered Sep 02 '21 at 10:42

Christoph Wintersteiger

8,234
1
16
30

Thank you, Christoph, am I right if I took one result with 'None' as an implicant? – QianruZhou Sep 05 '21 at 13:15

score 0 · Accepted Answer · answered Sep 02 '21 at 18:08

As Cristoph mentioned, if you are interested in complete enumeration, you want to make sure the "don't-care" assignments are always fixed at a particular value. To address the issue, you can use the following code:

from z3 import *
A1, B1, B2, C1, C2, E1, E2, F4 = Bools('A1 B1 B2 C1 C2 E1 E2 F4')
s = Solver()
s.add(simplify(Or(And(A1, Or(C1, C2), Or(B1, B2), E2, F4),.
    And(A1, C2, Or(B1, B2), E1))))

vars = [A1, B1, B2, C1, C2, E1, E2, F4]
while s.check() == sat:
    m = s.model()
    for v in vars:
      print("%s = %5s" % (v, m.evaluate(v, model_completion = True))),
    print
    s.add(Or([p != v for p, v in [(v, m.evaluate(v, model_completion = True)) for v in vars]]))

When run, this prints:

A1 =  True B1 =  True B2 = False C1 = False C2 =  True E1 =  True E2 =  True F4 =  True
A1 =  True B1 =  True B2 = False C1 = False C2 =  True E1 =  True E2 = False F4 = False
A1 =  True B1 =  True B2 =  True C1 = False C2 =  True E1 =  True E2 = False F4 = False
A1 =  True B1 = False B2 =  True C1 =  True C2 =  True E1 =  True E2 = False F4 = False
A1 =  True B1 =  True B2 =  True C1 =  True C2 =  True E1 =  True E2 = False F4 = False
A1 =  True B1 =  True B2 =  True C1 =  True C2 =  True E1 =  True E2 =  True F4 = False
A1 =  True B1 = False B2 =  True C1 = False C2 =  True E1 =  True E2 =  True F4 = False
A1 =  True B1 = False B2 =  True C1 =  True C2 =  True E1 =  True E2 =  True F4 = False
A1 =  True B1 = False B2 =  True C1 =  True C2 = False E1 = False E2 =  True F4 =  True
A1 =  True B1 =  True B2 = False C1 =  True C2 = False E1 = False E2 =  True F4 =  True
A1 =  True B1 =  True B2 = False C1 =  True C2 =  True E1 = False E2 =  True F4 =  True
A1 =  True B1 =  True B2 = False C1 =  True C2 =  True E1 =  True E2 = False F4 =  True
A1 =  True B1 =  True B2 = False C1 =  True C2 =  True E1 =  True E2 =  True F4 = False
A1 =  True B1 =  True B2 = False C1 =  True C2 =  True E1 =  True E2 =  True F4 =  True
A1 =  True B1 =  True B2 = False C1 = False C2 =  True E1 =  True E2 = False F4 =  True
A1 =  True B1 =  True B2 =  True C1 = False C2 =  True E1 =  True E2 = False F4 =  True
A1 =  True B1 =  True B2 =  True C1 =  True C2 =  True E1 =  True E2 = False F4 =  True
A1 =  True B1 = False B2 =  True C1 =  True C2 =  True E1 =  True E2 = False F4 =  True
A1 =  True B1 = False B2 =  True C1 =  True C2 = False E1 =  True E2 =  True F4 =  True
A1 =  True B1 =  True B2 = False C1 =  True C2 = False E1 =  True E2 =  True F4 =  True
A1 =  True B1 =  True B2 =  True C1 =  True C2 = False E1 = False E2 =  True F4 =  True
A1 =  True B1 =  True B2 =  True C1 =  True C2 = False E1 =  True E2 =  True F4 =  True
A1 =  True B1 =  True B2 = False C1 = False C2 =  True E1 = False E2 =  True F4 =  True
A1 =  True B1 = False B2 =  True C1 = False C2 =  True E1 = False E2 =  True F4 =  True
A1 =  True B1 = False B2 =  True C1 = False C2 =  True E1 =  True E2 = False F4 = False
A1 =  True B1 =  True B2 = False C1 =  True C2 =  True E1 =  True E2 = False F4 = False
A1 =  True B1 = False B2 =  True C1 =  True C2 =  True E1 = False E2 =  True F4 =  True
A1 =  True B1 =  True B2 =  True C1 = False C2 =  True E1 = False E2 =  True F4 =  True
A1 =  True B1 =  True B2 =  True C1 =  True C2 =  True E1 = False E2 =  True F4 =  True
A1 =  True B1 =  True B2 =  True C1 = False C2 =  True E1 =  True E2 =  True F4 = False
A1 =  True B1 =  True B2 = False C1 = False C2 =  True E1 =  True E2 =  True F4 = False
A1 =  True B1 = False B2 =  True C1 = False C2 =  True E1 =  True E2 =  True F4 =  True
A1 =  True B1 = False B2 =  True C1 =  True C2 =  True E1 =  True E2 =  True F4 =  True
A1 =  True B1 =  True B2 =  True C1 =  True C2 =  True E1 =  True E2 =  True F4 =  True
A1 =  True B1 =  True B2 =  True C1 = False C2 =  True E1 =  True E2 =  True F4 =  True
A1 =  True B1 = False B2 =  True C1 = False C2 =  True E1 =  True E2 = False F4 =  True

Which doesn't have any Nones or duplications.

Thank you very much, sorry I am new to this area. is that true that each results with 'none' is a implicant for the boolean formula? — QianruZhou, Sep 05 '21 at 13:22
No, it’s not necessarily an implicant. It just means that in that particular model, it’s value can be true or false, without affecting the satisfiability result. — alias, Sep 05 '21 at 17:00
I see, but the implicants (or even prime implicants) are among those with 'nones' (maybe those models with the most 'none' in it), is it correct? Thanks. — QianruZhou, Sep 05 '21 at 23:40
No, not necessarily. 'none's may or may not be implicants. The only conclusion you can draw is that its value is irrelevant to the satisfiability of the problem for that particular assignment. You cannot conclude anything else. To wit, consider a formula that doesn't mention a variable `x`. Assuming the formula is SAT, you'll get a model that assigns `none` as a value to `x` since it's not even mentioned. Obviously, `x` is not an implicant. (Prime or otherwise.) — alias, Sep 06 '21 at 00:41

why z3 solver give bool variable "none", how to get rid of it?

2 Answers2