本文介绍如何利用 z3 smt 求解器高效求解大规模线性布尔方程组（所有变量取值 ∈ {0,1}），替代传统暴力搜索或符号代数方法，完整演示建模、求解、遍历全部解的 python 实现，并分析不同位宽建模对解空间的影响。
本文介绍如何利用 z3 smt 求解器高效求解大规模线性布尔方程组（所有变量取值 ∈ {0,1}），替代传统暴力搜索或符号代数方法，完整演示建模、求解、遍历全部解的 python 实现，并分析不同位宽建模对解空间的影响。
在组合逻辑设计、密码分析、约束满足问题（CSP）及可满足性建模中，常需求解形如「多个 0–1 变量之和恒等于 1」的线性布尔方程组。这类问题本质是 0–1 整数线性方程组（0–1 ILP），变量数量达数十个时，穷举 $2^n$ 种组合不可行；而 SymPy 的 solve() 默认处理实数/符号域，无法原生支持整数约束与多解枚举——这正是 Z3 这类 SMT（Satisfiability Modulo Theories）求解器的核心优势场景。
Z3 支持精确建模布尔语义与整数约束。针对本题中 26 个变量（L/D/S 前缀）、12 个等式约束（每式和为 1），推荐采用 1-bit BitVec 建模：每个变量声明为 BitVec(name, 1)，其取值自动限定为 0 或 1，且加法按整数语义执行（非模 2），完美匹配题目要求。
以下是完整可运行的 Python 实现：
from z3 import Solver, BitVec, sat, Or
# 定义全部 26 个变量（按题目顺序）
var_names = 'L1 L2 L3 L4 L5 L6 L7 L8 S3 S5 S8 S9 S11 S12 S60 S72 S105 D4 D5 D8 D9 D10 D12 D16 D28 D72'.split()
params = [BitVec(name, 1) for name in var_names]
locals().update(zip(var_names, params)) # 动态注入变量名到局部作用域（便于写方程）
# 初始化求解器并添加 12 个约束方程
s = Solver()
s.add(L3 + L4 + S5 + S12 + L1 + D4 + L8 + S3 + L7 + D8 + D5 + L5 == 1)
s.add(L4 + D9 + S5 + L1 + D16 + L8 + L6 + S8 + L7 + D8 == 1)
s.add(L4 + L1 + D16 + S60 + L2 == 1)
s.add(L3 + D12 + L1 + S9 + S3 + D5 + S105 + L2 + L7 + D28 + L5 == 1)
s.add(S11 + L3 + S72 + D10 + D72 + D9 + S5 + D16 + S9 + S60 + L6 + S105 + L2 + L8 + D5 == 1)
s.add(L3 + S60 + L2 + L4 == 1)
s.add(D72 + L6 + S105 + L7 + D28 + L5 == 1)
s.add(S72 + D72 + L8 + L6 + L5 == 1)
s.add(D4 + S12 + S11 + D10 == 1)
s.add(D12 + D10 + S9 + S8 + D8 + S12 == 1)
s.add(S11 + D12 + S72 + D9 + D4 + S3 + S8 + D28 == 1)
s.add(S11 + D12 + D10 + D72 + D9 + D28 + S72 + S5 + S12 + D4 + D16 + S9 + S3 + S60 + S8 + S105 + D8 + D5 == 1)
# 枚举所有可行解
count = 0
while s.check() == sat:
count += 1
model = s.model()
# 格式化输出：变量名:取值（如 L1:1, S5:0）
solution_str = ", ".join([f"{v}:{model[v]}" for v in params])
print(f"Solution {count}: {solution_str}")
# 添加“排除当前解”的约束，确保下一轮找新解
s.add(Or([v != model[v] for v in params]))
print(f"\n✅ Total {count} distinct 0–1 solutions found.")✅ 关键技巧说明：
- BitVec(name, 1) 是最简洁的 0–1 建模方式，Z3 内部优化高效，无需额外 And(v >= 0, v
- s.add(Or([v != model[v] for v in params])) 是标准的「模型阻断（model blocking）」技术，强制下一次 check() 返回不同解；
- 若变量名含数字后缀（如 L1, S12），Z3 能正确解析，无需特殊转义。
⚠️ 注意事项与常见陷阱：
- 避免使用 Int() + 显式范围约束：若改用 Int('L1') 并添加 And(L1 >= 0, L1
- 勿混淆模 2 加法：本题是普通整数加法（如 1+1+0=2 ≠ 1），因此不能用 Xor 或 Bool 类型建模；
- 解空间爆炸预警：本例共找到数百个解（实际运行取决于方程组秩），若只需 一个 可行解，去掉 while 循环，仅调用一次 s.check() 即可；
- 扩展性提示：对超大规模问题（>100 变量），可结合 s.set(timeout=5000) 设置毫秒级超时，或使用 s.from_file("input.smt2") 导入 SMT-LIB 格式批量建模。
综上，Z3 不仅解决了原始 SymPy 方案无法处理整数约束与多解枚举的瓶颈，更以声明式语法大幅降低建模复杂度。对于任何需在 ${0,1}^n$ 空间中搜索满足线性等式/不等式约束的组合问题，Z3 都应作为首选工具链。
