如何为Z3 Solver添加约束：除一个变量外其余全为False？

首先，你当前的代码存在两个明显问题：

1. 变量列表里的f未定义，运行时会触发错误；
2. 循环给每个变量添加i==True约束，会强制所有变量都为True，完全违背你“仅有一个为True”的需求。

**不需要使用量词（Quantifier）**来实现这个需求，因为你的变量集合是有限的，直接通过简单的约束组合就能达成目标。以下是两种常用的实现方式：

方法一：利用布尔变量的整数特性求和 #

Z3允许将布尔变量当作整数处理（True对应1，False对应0），直接约束所有变量的和等于1即可：

from z3 import *

a, b, c, d = Bool('a'), Bool('b'), Bool('c'), Bool('d')
s = Solver()
all_vars = [a, b, c, d]
# 约束所有变量的和为1（恰好一个为True）
s.add(Sum([If(var, 1, 0) for var in all_vars]) == 1)

# 验证结果
if s.check() == sat:
    print(s.model())

方法二：逻辑析取组合 #

逐个指定“某变量为True，其余全为False”的情况，再将所有情况用逻辑或连接：

from z3 import *

a, b, c, d = Bool('a'), Bool('b'), Bool('c'), Bool('d')
s = Solver()
all_vars = [a, b, c, d]

# 生成每个变量为True且其他为False的约束，再取析取
exactly_one_true = Or([And(var, *[Not(other) for other in all_vars if other != var]) for var in all_vars])
s.add(exactly_one_true)

# 验证结果
if s.check() == sat:
    print(s.model())

两种方法都能实现“仅有一个布尔变量为True”的需求，其中方法一更简洁，尤其当变量数量较多时优势明显。

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