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。他们是独立的。如果要添加新子句，只需使用现有解算器，而不要创建新的解算器。