[FIXED] Z3Py solver producing different results in Jupyter

Issue

I'm learning how to use Z3Py through the Jupyter notebooks provided here, starting with guide.ipynb. I noticed something odd when running the below example code included in the Boolean Logic section.

p = Bool('p')
q = Bool('q')
r = Bool('r')
solve(Implies(p, q), r == Not(q), Or(Not(p), r))

The first time I run this in the Jupyter notebook it produces the result [p = False, q = True, r = False]. But if I run this code again (or outside of Jupyter) I instead get the result [q = False, p = False, r = True]

Am I doing something wrong to get these different results? Also, since the notebook doesn't say it, which solution is actually correct?

Solution

If you take both obtained results, i.e. assignments to your boolean variables, you'll see that each assignment set satisfies your constraints. Hence, both results are correct.

The fact that you obtain different results on different platforms/environments might be odd, but can be explained: SMT solvers typically use heuristics during their solving process, these are often randomised, and different environments may yield different random seeds.

Bottom line: it's all good :-)

Answered By - Malte Schwerhoff