Z3 是微软开发的 SMT（Satisfiability Modulo Theories）求解器，支持 Python API，可高效编码复杂约束谜题，如图着色、正则自动机与 N 皇后问题。这些谜题本质上是有限域变量间的关系约束，Z3 通过整数、数组、字符串理论直接建模，避免手动回溯搜索，实现快速求解。
图着色：关系约束编码
图着色问题是经典 NP 完全问题：给定无向图 G=(V,E) 与 k 色，要求相邻顶点不同色。用 Z3，定义每个顶点 v 的颜色变量 color [v] ∈ {0,1,...,k-1}，添加域约束与边约束。
核心代码框架：
from z3 import *
def graph_coloring(n_nodes, edges, k=3):
color = [Int(f'c_{i}') for i in range(n_nodes)]
s = Solver()
# 域约束
s.add([And(0 <= color[i], color[i] < k) for i in range(n_nodes)])
# 边约束：相邻不同色
s.add([color[u] != color[v] for u, v in edges])
# 对称打破：最小颜色为 0
s.add(color[0] == 0)
if s.check() == sat:
m = s.model()
return [m[color[i]].as_long() for i in range(n_nodes)]
return None
示例：4 节点环图 edges=[(0,1),(1,2),(2,3),(3,0)]，k=2 时 unsat（奇环），k=3 时 sat，返回 [0,1,0,2]。为求色数（chromatic number），二分搜索 k：低 1、高 Δ+1（最大度），每次 check。
落地参数：
- 超时：s = Solver (ctx=Context ((timeout=5000)))，单位 ms。
- 优化：若最小化最大色，用 o = Optimize ()，o.minimize (Max (color))。
- 监控：print (s.statistics ()) 查看 decisions、conflicts；>1e5 时重构模型（如用 BoolVector 位编码）。
此编码观点：关系直接转为！= 约束，Z3 整数理论高效传播。
正则转自动机：DFA 状态转移
正则填字（如 regex crosswords）中，行 / 列须匹配 regex。Z3 无内置 regex 解析，但支持 DFA 编码：预编译 regex 为 DFA（状态 S、转移 δ：S×Σ→S、接受 F），网格 char [r][c] ∈ {0..25}（A-Z）。
用 greenery 库转 DFA（pip install greenery），扁平转移表 transition [state][char_idx]。
import greenery # 辅助 regex → FSM
from z3 import *
def regex_row(length, pattern_str):
pat = greenery.parse(pattern_str).to_fsm()
n_states = len(pat.states)
ALPHABET_SIZE = 26
# 转移表（numpy 或 dict）
transition = ... # flatten as np.array(n_states, 26)
chars = IntVector('ch', length)
states = IntVector('st', length + 1)
s = Solver()
s.add([And(0 <= chars[i], chars[i] < ALPHABET_SIZE) for i in range(length)])
s.add([And(0 <= states[i], states[i] < n_states) for i in range(length + 1)])
s.add(states[0] == 0) # 起始状态
for i in range(length):
# 显式转移：If 阶梯避免 uninterpreted func 慢
next_st = If(states[i] == 0, If(chars[i] == 0, trans00, ...), ...) # 嵌套 If
s.add(states[i+1] == next_st)
s.add(Or([states[-1] == f for f in pat.finals]))
return s, chars, states
性能关键：用 Lambda 共享转移 expr，避免重复建树；预剪死状态（dead states 无接受路径）：
dead_chars = set(np.where((transition == dead_st).all(0))[0])
s.add([chars[i] != dc for dc in dead_chars for i in range(length)])
Nelhage 博客中，此法解 8x8 hex 网格 <30ms，原版>10s。Z3 regex 理论（Re ('a'), Concat, InRe）更简但慢 10x。
监控清单：
- 剪枝阈值：死字母 >50% 则用 EnumSort ('Char', ['A'..'Z']) 避整数算术。
- Tactics：s = Then ('macro-finder', 'qe', s) 展开 func 定义。
- 回滚：>1s 用 qflra-nlsat 策略（s = SolverFor ('QF_LRA')）。
N 皇后：增量求解与优化
N 皇后变体（如 LinkedIn Queens 加区域）：每行一皇后，不同列 / 对角 / 区域。IntVector 每行列位置。
from z3 import *
def n_queens(n, regions=None):
queens = IntVector('q', n)
s = Solver()
s.add([And(0 <= queens[i], queens[i] < n) for i in range(n)])
s.add(Distinct(queens)) # 不同列
# 对角：非邻接变体 Abs(qi - qj) != |i-j|
for i in range(n):
for j in range(i+1, n):
s.add(queens[i] - queens[j] != i - j)
s.add(queens[i] - queens[j] != j - i)
if regions: # 每区域至少一皇后
for reg in regions:
s.add(Or([Implies(And(i == r[0], queens[i] == r[1]), True) for r in reg]))
return s.check(), s.model()
增量：多线索谜题，初始 s.check () 得部分解，后续 s.push ()；s.add (new_constraint)；s.check ()。优化：o = Optimize ()，o.maximize (sum 得分) 或 o.minimize (conflicts)。
Hillel Wayne 示例中，区域 Or ([queens [row]==col for (row,col) in reg]) 确一皇后 / 区。9x9 <1s。
参数清单：
- 增量深度：push/pop 栈 >10 则新 Solver ()。
- Opt：o.check ([constraints]) 带额外。
- 超时 / 并行：ctx = Context (num_threads=4, timeout=10000)。
- 风险限：n>20 用 bitvec (BV (n)) 编码位置，SolverFor ('QF_BV')。
工程化实践
统一流程：1) 变量域（Int/Enum）；2) 关系（!=, Distinct, If 转移）；3) 剪枝（死分支、对称固定）；4) 增量 check；5) 模型读出 m.eval (var)。
性能不稳：优先 EnumSort 避 arith；Lambda/forall+macro-finder 共享 expr；域分析剪 50% 搜索空间。测试：Advent of Code Z3 仓库验证。
资料来源：
- Hillel Wayne: https://www.hillelwayne.com/post/z3-examples/ （Z3 脚本示例）
- Nelhage: https://blog.nelhage.com/post/regex-crosswords-z3/ （DFA 性能优化）
- Wayne Queens: https://buttondown.com/hillelwayne/archive/solving-linkedin-queens-with-smt/
（正文 1250+ 字）