第四章：基于UNSAT核心的定位
什么是UNSAT核心？
先问个问题：你写了一大堆约束条件，求解器告诉你「不可满足」。这时候你最想知道什么？
说白了，你需要的不是「不行」这两个字，而是「哪里不行」。UNSAT核心就是干这个的。
UNSAT核心，是导致整个约束系统不可满足的那一小部分约束子集。举个例子：
约束1：x > 5
约束2：x < 3
约束3：y = 10
约束4：z ≠ z这里约束1和约束2放在一起就矛盾了，它们俩就是一个UNSAT核心。约束3和约束4虽然也有问题，但跟核心矛盾无关。
我刚开始做形式化验证时，遇到不可满足就傻眼。后来发现，UNSAT核心就像调试时的断点——它告诉你矛盾在哪里，而不是让你满世界找。
最小冲突集（MCS）
UNSAT核心有个更严格的版本——最小冲突集（Minimal Unsatisfiable Subset, MUS）。
MUS的特点是：
- 它本身不可满足
- 去掉其中任意一个约束，剩下的就变成可满足
- 它是最「精简」的矛盾描述
你想想看，如果UNSAT核心有10个约束，但其中5个是多余的，那定位起来还是费劲。MUS就是要找到那个「刚刚好」的矛盾集合。
如何提取UNSAT核心？
提取UNSAT核心，主流方法有三种：
- 删除法（Deletion-based）：逐个删除约束，检查剩余集合是否仍然不可满足
- 插入法（Insertion-based）：从空集开始，逐个添加约束，直到出现矛盾
- 基于证明的分析：直接从求解器的证明日志中提取核心
我个人最常用的是删除法。原因很简单——它直观，不容易出错。
删除法的伪代码：
输入：约束集合 C = {c1, c2, ..., cn}
输出：UNSAT核心 U
U = C // 初始化为全部约束
for each ci in C:
if (U \ {ci}) 不可满足:
U = U \ {ci} // 去掉ci后仍然矛盾，说明ci不是必要的
return U工具实践：Z3
Z3是微软出品的SMT求解器，提取UNSAT核心非常方便。来看个例子：
from z3 import *
# 创建求解器，开启核心提取
s = Solver()
s.set(unsat_core=True)
# 创建变量
x = Int('x')
y = Int('y')
# 添加带标签的约束
s.assert_and_track(x > 5, "c1")
s.assert_and_track(x < 3, "c2")
s.assert_and_track(y == 10, "c3")
# 求解
result = s.check()
if result == unsat:
core = s.unsat_core()
print("UNSAT核心:", core)
# 输出: [c1, c2]这里的关键是assert_and_track函数。它给每个约束打上标签，求解器就能告诉你哪些标签对应的约束在核心中。
unsat_core=True。结果调用unsat_core()时直接报错。嗯，这个坑我踩过，你记住就好。
工具实践：MiniSAT
MiniSAT是经典的SAT求解器，提取UNSAT核心需要一点额外工作。它本身不直接支持核心提取，但可以通过修改源码或使用扩展版本实现。
MiniSAT的UNSAT核心提取流程：
// 伪代码：MiniSAT核心提取
1. 将每个子句（约束）编号
2. 求解原始问题
3. 如果不可满足，进入核心提取模式
4. 对每个子句：
- 暂时移除该子句
- 重新求解
- 如果仍然不可满足，永久移除该子句
- 否则，保留该子句
5. 剩余的子句就是UNSAT核心我建议使用MiniSAT+或PicoSAT，它们原生支持核心提取，省去自己实现的麻烦。
| 工具 | 核心提取支持 | 适用场景 | 我的评价 |
|---|---|---|---|
| Z3 | 原生支持 | SMT问题、混合约束 | 最推荐，API友好 |
| MiniSAT | 需扩展 | 纯SAT问题 | 性能好，但配置麻烦 |
| PicoSAT | 原生支持 | 纯SAT问题 | 轻量级，适合嵌入式 |
核心提取的流程图
下面这张图展示了UNSAT核心提取的完整流程：
实际项目中的经验
我在一个工业级项目中遇到过这样的情况：一个硬件验证模型有5000多条约束，求解器跑了3分钟才说「不可满足」。用删除法提取核心，花了将近2小时。但核心只有8条约束——其中一条是类型定义错误，另一条是时序约束写反了。
嗯，这里要注意：核心提取的时间成本。如果约束集很大，建议先用启发式方法缩小范围，再提取核心。
我的建议：
- 约束数量 < 100：直接提取核心，很快
- 约束数量 100-1000：用删除法，可以接受
- 约束数量 > 1000：先用分组策略，再对可疑组提取核心
最后说一句：别指望UNSAT核心能自动修复问题。它只是告诉你「矛盾在这里」，至于怎么解决，还得靠你的领域知识和逻辑推理。工具是辅助，人才是主角。