与 Z3 Python API 进行异或 - 仅返回单个解决方案

Question

我正在使用 Z3 的 Python API 测试单个 XOR 语句。

这是我得到的输出：

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

但是，我应该有 3 个解决方案，其中两个变量为 false，最后一个为 true。我哪里出错了？

from z3 import *

A_L = Bool('A_L')
A_M = Bool('A_M')
A_R = Bool('A_R')

B_L = Bool('B_L')
B_M = Bool('B_M')
B_R = Bool('B_R')

C_L = Bool('C_L')
C_M = Bool('C_M')
C_R = Bool('C_R')

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

if s.check() == sat:
    m = s.model()
    print(m)
else:
    print("invalid installation profile")

Answer 1

您刚刚得到三个解决方案中的第一个。
原因是，您的代码不会寻找替代代码。

正如这篇文章中所解释的，您应该添加阻止先前解决方案的约束。
然后，重新运行求解器以获得其他解决方案。

from z3 import *

A_L = Bool('A_L')
A_M = Bool('A_M')
A_R = Bool('A_R')

B_L = Bool('B_L')
B_M = Bool('B_M')
B_R = Bool('B_R')

C_L = Bool('C_L')
C_M = Bool('C_M')
C_R = Bool('C_R')

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

#  https://brandonrozek.com/blog/obtaining-multiple-solutions-z3/
def get_solutions(s: z3.z3.Solver):
    result = s.check()
    # While we still get solutions
    while (result == z3.sat):
      m = s.model()
      yield m
      # Add new solution as a constraint
      block = []
      for var in m:
          block.append(var() != m[var])
      s.add(z3.Or(block))
      # Look for new solution
      result = s.check()

s = Solver()

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

solutions = get_solutions(s)
upper_bound = 10
for solution, _ in zip(solutions, range(upper_bound)):
    print(solution)

事实上有更复杂、更有效的方法来获得多种解决方案。这些内容在here有描述。