Z3-Python 因为 SAT 求解器没有给出正确的结果

Question

我正在尝试使用 Z3（在 Python 中）作为 SAT 求解器，但结果出乎意料。

首先，假设我想获得以下公式的模型：

from z3 import *

c_0 = Bool('c_0')
c_1 = Bool('c_1')
c_2 = Bool('c_2')
c_3 = Bool('c_3')

sss = Solver()
negations = And(Not(c_0), Not(c_1), Not(c_2), Not(c_3))
sss.add(Not(negations))
print(sss.check())
print(sss.model())

所以我得到 sat，模型 [c_0 = True, c_3 = False, c_1 = False, c_2 = False]，它包含公式（我不知道为什么变量赋值是按那个顺序给出的）。

但是现在，我在公式中添加And(Not(c_1), Not(c_2), Not(c_3))（不需要理解为什么）。然后我得到结果unsat，这是没有意义的。结果应该是 sat，例如，模型 [c_0 = True, c_1 = False, c_2 = True, c_3 = False].

代码如下：

added_negations = And(Not(c_1), Not(c_2), Not(c_3))
new_Negations = And(negations, Not(added_negations))

ss = Solver()
ss.add(new_Negations)
print(new_Negations)
print(ss.check())

有什么帮助吗？我使用显式 Exists(c_0,c_1...) 对此进行了测试，但结果是一样的。

我犯了一个错误！！！

new_Negations = And(negations, Not(added_negations)) 中缺少一个否定。正确：new_Negations = And(Not(negations), Not(added_negations))

更正这个，结果又是sat，具体来说，模型是：[c_0 = False, c_3 = False, c_1 = True, c_2 = False]

Answer 1

您创建了两个求解器，一个名为 ss，另一个名为 sss。他们是独立的。如果要添加新的子句，只需使用现有的求解器，不要创建新的。

Z3-Python 因为 SAT 求解器没有给出正确的结果

Z3-Python as SAT solver does not give right results

satisfiability

smt

z3

z3py

sat