while enumerating Z3 solutions, model does not give value for variable

Question

I'm new to using Z3 but I am seeing some strange behavior when trying to enumerate solutions to a set of boolean constraints. My code is below:

from z3 import Bool, Xor, Or, And, Not, Solver, sat

x0 = Bool("x0")
x1 = Bool("x1")
x2 = Bool("x2")
x3 = Bool("x3")

solver = Solver()
solver.add(Xor(x0, x1))
solver.add(Xor(Or(x2, x0), Not(x3)))

while solver.check() == sat:
    model = solver.model()
    print()
    print(solver)
    print(model)
    cons = Or([d() != model[d] for d in model])
    solver.add(cons)

Which outputs


[Xor(x0, x1), Xor(Or(x2, x0), Not(x3))]
[x3 = False, x2 = False, x1 = True, x0 = False]

[Xor(x0, x1),
 Xor(Or(x2, x0), Not(x3)),
 Or(x3 != False, x2 != False, x1 != True, x0 != False)]
[x3 = True, x1 = False, x0 = True]

[Xor(x0, x1),
 Xor(Or(x2, x0), Not(x3)),
 Or(x3 != False, x2 != False, x1 != True, x0 != False),
 Or(x3 != True, x1 != False, x0 != True)]
[x3 = True, x2 = True, x1 = True, x0 = False]

You can see that the second model gives [x3 = True, x1 = False, x0 = True] with no reference to the value of x2 even though x2 clearly has constraints in the solver.

But Or(x3 != False, x2 != False, x1 != True, x0 != False) should not eliminate any one variable, necessarily. It just means one of them must change. — Cory Nezin, May 20 '21 at 16:10
In your source `x2` only goes into `Or(x2, x0)` . Solver says `x0=True` this is effectively then `Or(x2, True)` and that simplifies into just `True`. — fukanchik, May 20 '21 at 16:12
Try it yourself. Take solver's solution and then test two cases - one with x2=False and another one with x2=True. — fukanchik, May 20 '21 at 16:13
That `Or` you are referring to is nested in an `Xor` so I don't think it's that simple. Even assuming it is 'eliminated' shouldn't the model still give some result? Can I force that? My goal is to iterate over all solutions so I would like to force an answer. — Cory Nezin, May 20 '21 at 16:16
I am not sure what you mean by "force". Whenever you get solution without a variable - you are free to use whatever in that place. Just always use False, or True. — fukanchik, May 20 '21 at 16:18
use SimpleSolver then instead. It prints for me all possible solutions including redundant ones. — fukanchik, May 20 '21 at 16:24
Can you give some example code? I don't see many docs for that. But anyway I figured a way to do it in my answer. — Cory Nezin, May 20 '21 at 16:26
Replace `solver = Solver()` with `solver = SimpleSolver()` and it will output what you want. — fukanchik, May 20 '21 at 16:28
That fixes the second case though the final case still excludes x2 — Cory Nezin, May 20 '21 at 16:31
This is output which I get: `{x0: False, x1: True, x2: False, x3: False} {x0: False, x1: True, x2: True, x3: True} {x0: True, x1: False, x2: True, x3: True} {x0: True, x1: False, x2: False, x3: True} ` all the vars are in place. — fukanchik, May 20 '21 at 16:33

score 2 · Answer 1 · answered May 20 '21 at 16:24

This can be solved by using model_completion in order to fill an arbitrary value for a free variable.

from z3 import Bool, Xor, Or, And, Not, Solver, sat

x0 = Bool("x0")
x1 = Bool("x1")
x2 = Bool("x2")
x3 = Bool("x3")
refs = [x0, x1, x2, x3]

solver = Solver()
solver.add(Xor(x0, x1))
solver.add(Xor(Or(x2, x0), Not(x3)))

while solver.check() == sat:
    model = solver.model()
    print({d: model.eval(d, model_completion=True) for d in refs})
    cons = Or([d != model.eval(d, model_completion=True) for d in refs])
    solver.add(cons)

{x0: False, x1: True, x2: False, x3: False}
{x0: False, x1: True, x2: True, x3: True}
{x0: True, x1: False, x2: False, x3: True}
{x0: True, x1: False, x2: True, x3: True}

This has been discussed on SO before. See here: https://stackoverflow.com/questions/53162290/why-z3py-does-not-provide-all-possible-solutions for instance. — alias, May 20 '21 at 17:01

while enumerating Z3 solutions, model does not give value for variable

1 Answers1