将 true 分配给除 one 之外的所有变量

Question

我有一个变量列表，我想向 z3 求解器添加约束，例如所有变量都应该是 False，除了一个变量应该是 True ..

a,b,c,d= Bool('a,b,c,d')
s = Solver()
allvariables=[a,b,c,d,f] 
for i in allvariables:
     s.add(i==True)
     

我需要使用量词吗？

Answer 1

有多种方法来编写此约束，但使用起来最简单（也是最高效）的方法可能是 PbEq：

from z3 import *

a, b, c, d = Bools("a b c d")
allVars = [a, b, c, d]

s = Solver()
s.add(PbEq([(v, 1) for v in allVars], 1))

while s.check() == sat:
    m = s.model()
    print(m)
    s.add(Not(And(m[a] == a, m[b] == b, m[c] == c, m[d] == d)))

这打印：

[b = False, a = True, c = False, d = False]
[b = True, a = False, c = False, d = False]
[b = False, a = False, c = True, d = False]
[b = False, a = False, c = False, d = True]