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

Question

我正在通过提供的Jupyter笔记本学习如何使用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

如果你把两个得到的结果，即对你的布尔变量的赋值，你会看到每个赋值集都满足你的约束。因此，两个结果都是正确的。

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

一句话：这都是好的:-)