Z3Py求解器在Jupyter中产生不同的结果

Question

我正在学习如何通过here提供的Jupyter notebooks使用Z3Py，从guide.ipynb开始。在运行布尔逻辑部分中包含的以下示例代码时，我注意到了一些奇怪的事情。

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

我第一次在Jupyter笔记本中运行它时，它会生成结果[p = False, q = True, r = False]。但是如果我再次运行这段代码(或者在Jupyter之外)，我得到的结果是[q = False, p = False, r = True]

为了得到这些不同的结果，我做错了什么吗？另外，既然笔记本上没有说明，那么哪种解决方案才是正确的呢？

Answer 1

如果你获得了两个结果，也就是对布尔变量的赋值，你会发现每个赋值集都满足你的约束条件。因此，这两个结果都是正确的。

在不同的平台/环境上获得不同的结果可能很奇怪，但可以解释: SMT解算器通常在其求解过程中使用启发式，这些启发式通常是随机的，并且不同的环境可能会产生不同的随机种子。

结论:一切都很好:-)