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?

Improve this question

1 Answer 1

Reset to default
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 :-)

Improve this answer
Sign up to request clarification or add additional context in comments.

2 Comments

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?
@JAKZero AFAIK, manual iteration is the only way to obtain all possible solutions

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.