为什么Z3求解器返回布尔变量为None？如何解决该问题及重复模型

问题原因 #

1. None值产生原因 #

Z3求解器默认仅返回满足约束必需的变量赋值，对于取值不影响公式可满足性的变量，不会主动分配布尔值，直接通过model[变量名]访问未赋值变量就会得到None。

2. 重复模型产生原因 #

你构造阻塞约束时，使用了值为None的变量参与比较，导致阻塞约束逻辑不完整，无法正确排除上一次得到的可满足赋值组合，求解器下一次校验时会再次返回结构几乎一致的模型，因此出现大量重复输出。

解决方法 #

使用Z3模型的eval()方法，设置model_completion=True参数，自动为未赋值的变量补全布尔值（默认补False，不影响枚举完整性），再用补全后的取值构造阻塞约束即可。
修改后的代码如下：

from z3 import *
# 统一管理所有布尔变量
vars_list = [A1, B1, B2, C1, C2, E1, E2, F4] = Bools('A1 B1 B2 C1 C2 E1 E2 F4')
s = Solver()
s.add(Or(And(A1, Or(C1, C2), Or(B1, B2), E2, F4), 
        And(A1, C2, Or(B1, B2), E1)))

while s.check() == sat:
    m = s.model()
    # 补全所有变量的赋值，消除None
    completed_vals = [m.eval(var, model_completion=True) for var in vars_list]
    # 输出所有变量的布尔值
    print([str(val) for val in completed_vals])
    # 构造阻塞约束，排除当前完整赋值组合
    block = [var != val for var, val in zip(vars_list, completed_vals)]
    s.add(Or(block))

运行修改后的代码，输出的所有变量仅会出现True/False两种取值，且每个赋值组合仅输出一次，无重复。

内容的提问来源于stack exchange，提问作者QianruZhou