0

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?

JAK Zero
  • 301
  • 6
  • 13

1 Answers1

1

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 :-)

Malte Schwerhoff
  • 12,684
  • 4
  • 41
  • 71
  • It's good to hear that `solve()` only prints a single solution, I was worried I had broken something. Is there any built-in functionality for printing all possible solutions, or would I have to do something like what is shown in [this answer](https://stackoverflow.com/a/53163796/8031185)? – JAK Zero May 20 '20 at 09:01
  • 1
    @JAKZero AFAIK, manual iteration is the only way to obtain all possible solutions – Malte Schwerhoff May 24 '20 at 12:50