使用Z3 Python API求解异或问题仅返回单个解，求助排查

你遇到的问题并非代码逻辑错误，而是Z3求解器的默认行为导致的：Z3找到第一个满足约束的模型后就会停止，不会主动返回所有可能的解。你的XOR函数逻辑是正确的（定义了“恰好一个变量为真”的情况，对应三个解），但当前代码仅获取了第一个解。

错误原因 #

你的代码只调用了一次s.check()和s.model()，而Z3默认仅返回单个满足条件的模型，而非全部解。要获取所有三个符合要求的解，需要循环迭代求解，每次找到解后添加约束排除该解，直到求解器返回unsat（无解）。

修正后的代码 #

from z3 import *

A_L = Bool('A_L')
B_L = Bool('B_L')
C_L = Bool('C_L')

def OnlyA(a,b,c):
    return And(a, Not(b), Not(c))

def XOR(a,b,c):
    return Or(OnlyA(a,b,c), OnlyA(b,c,a), OnlyA(c,b,a))

s = Solver()
s.add(XOR(A_L, B_L, C_L))

# 循环获取所有解
solutions = []
while s.check() == sat:
    m = s.model()
    solutions.append(m)
    # 添加约束排除当前解
    block = []
    for var in m:
        block.append(var() != m[var])
    s.add(Or(block))

# 输出所有解
for sol in solutions:
    print(sol)

输出结果 #

运行修正后的代码，会得到所有三个符合要求的解：

[B_L = True, A_L = False, C_L = False]
[A_L = True, B_L = False, C_L = False]
[C_L = True, A_L = False, B_L = False]

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