为什么 z3 求解器给出 bool 变量 "none"，如何摆脱它？

Question

我是 Z3py 的新手。我正在尝试列出布尔公式的所有满意解决方案（或获取仅生成 True 的真相 table）。

我的代码在这里，灵感来自另一个答案finding all satisfying models:

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
...

如你所见，他们有重复的结果，其中有“None”，为什么会这样？ Bool 变量不是只有“真”或“假”吗？为什么里面有重复的模型？非常感谢。

Answer 1

None 是无关紧要的；这意味着您可以自由选择 True 或 False，两者都是有效模型。您可以要求 Z3 通过启用模型完成来填写这些值，例如在

中完成的

Answer 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

其中没有任何 None 或重复项。

为什么 z3 求解器给出 bool 变量 "none"，如何摆脱它？

why z3 solver give bool variable "none", how to get rid of it?

boolean-logic

truthtable

boolean-operations

z3

z3py