提问人：QianruZhou 提问时间：9/2/2021 更新时间：9/3/2021 访问量：311
为什么 Z3 求解器给布尔变量“无”，如何摆脱它？
why z3 solver give bool variable "none", how to get rid of it?
问：
我是 Z3py 的新手。我正在尝试列出布尔公式的所有满意解决方案（或获得仅生成 True 的真值表）。
我的代码在这里，灵感来自另一个答案，找到所有令人满意的模型：
from z3 import *
A1, B1, B2, C1, C2, E1, E2, F4 = Bools('A1 B1 B2 C1 C2 E1 E2 F4')
s = Solver()
s.add(simplify(Or(And(A1, Or(C1, C2), Or(B1, B2), E2, F4),
And(A1, C2, Or(B1, B2), E1))))
while s.check() == sat:
print(s.model())
s.add(Or(A1 != s.model()[A1],
B1 != s.model()[B1],
B2 != s.model()[B2],
C1 != s.model()[C1],
C2 != s.model()[C2],
E1 != s.model()[E1],
E2 != s.model()[E2],
F4 != s.model()[F4]))
但我得到的结果是这样的：
True,True,None,None,True,True,False,None
True,True,None,None,True,True,False,None
True,True,None,None,True,True,False,None
True,True,None,None,True,True,False,None
...
如您所见，它们有重复的结果，并且其中有“无”，为什么会这样？布尔变量只有“true”或“false”是真的吗？为什么里面有重复的模型？谢谢。
答：
1赞
Christoph Wintersteiger
9/2/2021
#1
None是不在乎的;这意味着您可以自由选择其中之一，或者两者都是有效的模型。您可以要求 Z3 通过启用模型完成来填充这些值，例如，在如何在 Z3py 中建模中完成TrueFalse
评论
0赞
QianruZhou
9/5/2021
谢谢你，克里斯托夫，如果我以“无”为隐含物，我是对的吗？
0赞
alias
9/3/2021
#2
正如 Cristoph 所提到的，如果你对完整枚举感兴趣，你要确保“不关心”赋值始终固定在一个特定的值上。若要解决此问题，可以使用以下代码：
from z3 import *
A1, B1, B2, C1, C2, E1, E2, F4 = Bools('A1 B1 B2 C1 C2 E1 E2 F4')
s = Solver()
s.add(simplify(Or(And(A1, Or(C1, C2), Or(B1, B2), E2, F4),.
And(A1, C2, Or(B1, B2), E1))))
vars = [A1, B1, B2, C1, C2, E1, E2, F4]
while s.check() == sat:
m = s.model()
for v in vars:
print("%s = %5s" % (v, m.evaluate(v, model_completion = True))),
print
s.add(Or([p != v for p, v in [(v, m.evaluate(v, model_completion = True)) for v in vars]]))
运行时，这将打印：
A1 = True B1 = True B2 = False C1 = False C2 = True E1 = True E2 = True F4 = True
A1 = True B1 = True B2 = False C1 = False C2 = True E1 = True E2 = False F4 = False
A1 = True B1 = True B2 = True C1 = False C2 = True E1 = True E2 = False F4 = False
A1 = True B1 = False B2 = True C1 = True C2 = True E1 = True E2 = False F4 = False
A1 = True B1 = True B2 = True C1 = True C2 = True E1 = True E2 = False F4 = False
A1 = True B1 = True B2 = True C1 = True C2 = True E1 = True E2 = True F4 = False
A1 = True B1 = False B2 = True C1 = False C2 = True E1 = True E2 = True F4 = False
A1 = True B1 = False B2 = True C1 = True C2 = True E1 = True E2 = True F4 = False
A1 = True B1 = False B2 = True C1 = True C2 = False E1 = False E2 = True F4 = True
A1 = True B1 = True B2 = False C1 = True C2 = False E1 = False E2 = True F4 = True
A1 = True B1 = True B2 = False C1 = True C2 = True E1 = False E2 = True F4 = True
A1 = True B1 = True B2 = False C1 = True C2 = True E1 = True E2 = False F4 = True
A1 = True B1 = True B2 = False C1 = True C2 = True E1 = True E2 = True F4 = False
A1 = True B1 = True B2 = False C1 = True C2 = True E1 = True E2 = True F4 = True
A1 = True B1 = True B2 = False C1 = False C2 = True E1 = True E2 = False F4 = True
A1 = True B1 = True B2 = True C1 = False C2 = True E1 = True E2 = False F4 = True
A1 = True B1 = True B2 = True C1 = True C2 = True E1 = True E2 = False F4 = True
A1 = True B1 = False B2 = True C1 = True C2 = True E1 = True E2 = False F4 = True
A1 = True B1 = False B2 = True C1 = True C2 = False E1 = True E2 = True F4 = True
A1 = True B1 = True B2 = False C1 = True C2 = False E1 = True E2 = True F4 = True
A1 = True B1 = True B2 = True C1 = True C2 = False E1 = False E2 = True F4 = True
A1 = True B1 = True B2 = True C1 = True C2 = False E1 = True E2 = True F4 = True
A1 = True B1 = True B2 = False C1 = False C2 = True E1 = False E2 = True F4 = True
A1 = True B1 = False B2 = True C1 = False C2 = True E1 = False E2 = True F4 = True
A1 = True B1 = False B2 = True C1 = False C2 = True E1 = True E2 = False F4 = False
A1 = True B1 = True B2 = False C1 = True C2 = True E1 = True E2 = False F4 = False
A1 = True B1 = False B2 = True C1 = True C2 = True E1 = False E2 = True F4 = True
A1 = True B1 = True B2 = True C1 = False C2 = True E1 = False E2 = True F4 = True
A1 = True B1 = True B2 = True C1 = True C2 = True E1 = False E2 = True F4 = True
A1 = True B1 = True B2 = True C1 = False C2 = True E1 = True E2 = True F4 = False
A1 = True B1 = True B2 = False C1 = False C2 = True E1 = True E2 = True F4 = False
A1 = True B1 = False B2 = True C1 = False C2 = True E1 = True E2 = True F4 = True
A1 = True B1 = False B2 = True C1 = True C2 = True E1 = True E2 = True F4 = True
A1 = True B1 = True B2 = True C1 = True C2 = True E1 = True E2 = True F4 = True
A1 = True B1 = True B2 = True C1 = False C2 = True E1 = True E2 = True F4 = True
A1 = True B1 = False B2 = True C1 = False C2 = True E1 = True E2 = False F4 = True
它没有任何 s 或重复项。None
评论
0赞
QianruZhou
9/5/2021
非常感谢，对不起，我是这个领域的新手。每个带有“无”的结果都是布尔公式的隐含物，这是真的吗？
0赞
alias
9/6/2021
不，它不一定是隐含的。它只是意味着在该特定模型中，它的值可以是真或假，而不会影响满足性结果。
0赞
QianruZhou
9/6/2021
我明白了，但是隐含物（甚至是主要隐含物）属于具有“无”的模型（也许是其中“无”最多的模型），这是正确的吗？谢谢。
0赞
alias
9/6/2021
不，不一定。“没有”可能是也可能不是隐含物。您可以得出的唯一结论是，它的值与该特定赋值的问题的满足性无关。你不能得出其他任何结论。举个例子，考虑一个没有提到变量的公式。假设公式是 SAT，您将得到一个作为值分配的模型，因为它甚至没有被提及。显然，不是隐含者。（Prime 或其他。xnonexx
评论