[INFO] SAT/SMT算法详解：自动推理的核心技术

时间: 2024-12-19
类型: 算法详解
来源: 技术深度讲解
置信度: 9/10
标签: #SAT #SMT #CDCL #DPLL #算法 #形式化验证

SAT：布尔可满足性问题

定义

要素	说明
输入	由布尔变量（x, y, z）+ 逻辑运算符（AND, OR, NOT）组成的公式
输出	存在使公式为真的赋值 → SAT；否则 → UNSAT
重要性	第一个被证明的NP完全问题，是验证和推理问题的基础

CDCL算法：冲突驱动子句学习

def cdcl_solver(formula):
    decisions = []       # 决策栈
    assignment = {}      # 当前赋值
    clause_db = formula  # 子句数据库

    while True:
        # 1. 布尔约束传播（BCP）
        conflict_clause = unit_propagation(clause_db, assignment)

        if conflict_clause is not None:
            if decisions == []:
                return UNSAT  # 冲突且无法回溯

            # 2. 冲突分析：学习新子句
            learned_clause, backtrack_level = analyze_conflict(conflict_clause)
            clause_db.append(learned_clause)

            # 3. 回溯
            backtrack(backtrack_level, decisions, assignment)
        else:
            if all_variables_assigned(assignment):
                return SAT  # 找到解

            # 4. 决策：选择未赋值的变量
            var, value = make_decision(clause_db, assignment)
            decisions.append((var, value))
            assignment[var] = value

CDCL四大组件

组件	功能
布尔约束传播(BCP)	识别单位子句，强制赋值
冲突分析	分析冲突原因，学习新子句，避免重复错误
回溯	回到冲突发生前的某个决策点
决策启发式(VSIDS)	优先选择近期冲突中频繁出现的变量

SAT示例

公式：(A ∨ ¬B) ∧ (¬A ∨ C) ∧ (B ∨ ¬C)

求解过程：

决策：选择A=True
传播：
- (A∨¬B) 已满足
- (¬A∨C) 要求 C=True
- (B∨¬C) 由于C=True，要求B=True
赋值：{A=True, B=True, C=True}
验证：所有子句满足 → SAT

SMT：可满足性模理论

定义

要素	说明
核心思想	SAT的扩展，在特定理论下判断一阶逻辑公式的可满足性
优势	能处理算术、数组、位向量等复杂理论
架构	SAT求解器 + 理论求解器(T-solver)协作

DPLL(T)框架

def dpll_t_solver(smt_formula):
    # 1. 抽象：将理论原子替换为布尔变量
    bool_abstraction, atom_map = abstract_to_propositional(smt_formula)

    while True:
        # 2. SAT求解器寻找布尔模型
        sat_result, bool_model = sat_solver(bool_abstraction)

        if sat_result == UNSAT:
            return UNSAT

        # 3. 具体化：将布尔模型转换为理论约束
        theory_constraints = concretize(bool_model, atom_map)

        # 4. 理论求解器检查理论一致性
        t_result, conflict = t_solver(theory_constraints)

        if t_result == SAT:
            return SAT  # 找到完整解
        else:
            # 5. 学习理论冲突子句，反馈给SAT求解器
            learned_clause = generate_theory_lemma(conflict, atom_map)
            bool_abstraction.add_clause(learned_clause)

DPLL(T)工作流程

SMT公式 → [抽象] → 布尔公式
              ↓
         [SAT求解]
              ↓
         布尔模型 → [具体化] → 理论约束
                               ↓
                          [理论求解]
                               ↓
                    SAT ← 一致 / 冲突 → 学习新子句 → 循环

SMT示例：线性算术理论

公式：(x + y > 5) ∧ (x - y < 1) ∧ (x > 0)

求解过程：

抽象：
- P₁: x + y > 5
- P₂: x - y < 1
- P₃: x > 0
- 布尔公式：P₁ ∧ P₂ ∧ P₃
SAT求解：{P₁=True, P₂=True, P₃=True}
理论检查：
- 约束：{x+y>5, x-y<1, x>0}
- 求解：x=3, y=3
- 验证：3+3=6>5 ✓, 3-3=0<1 ✓, 3>0 ✓
结果：SAT

SMT示例：数组理论

公式：(store(A, i, v)[j] = v) ∧ (i ≠ j) ∧ (select(A, j) ≠ v)

数组公理：

select(store(A, i, v), i) = v（写后读相同）
select(store(A, i, v), j) = select(A, j) 当 i ≠ j（写后读不同）

推理：

由于 i≠j：store(A, i, v)[j] = select(A, j)
但公式要求 store(A, i, v)[j] = v 且 select(A, j) ≠ v
矛盾！→ UNSAT

SAT vs SMT 对比

特性	SAT	SMT
输入	命题逻辑公式	一阶逻辑公式 + 理论
理论支持	无	算术、数组、位向量等
表达能力	较弱	很强
求解架构	CDCL	DPLL(T)
应用场景	硬件验证、规划	程序验证、符号执行

支持的理论

理论	处理内容
线性算术(LIA/LRA)	整数/实数的加减比较
位向量(BV)	固定宽度二进制运算
数组(Array)	select/store操作
未解释函数(UF)	函数等式推理
字符串(String)	字符串操作和约束

主流求解器

求解器	特点
Z3	微软出品，最广泛使用，API丰富
CVC5	斯坦福/爱荷华，证明能力强
MiniSat	轻量级SAT求解器
Yices	高性能SMT

实际应用场景

场景	应用
程序验证	验证程序断言是否总是成立
符号执行	探索程序所有执行路径
编译器优化	验证优化变换的正确性
AI规划	寻找满足约束的行动序列
测试生成	生成覆盖特定路径的测试输入

核心洞察

SAT/SMT求解器就像计算机的"自动数学家"——能够系统地探索巨大的搜索空间，为形式化验证和智能推理提供坚实的技术基础。

CDCL的核心智慧：

不是盲目搜索，而是从错误中学习
学到的子句避免重复犯同样的错误
类似于人类的"经验总结"

关联

相关: INFO-20251219-036（判定过程与AI Agent，应用层面）
相关: INFO-20251219-025（状态空间理论，决策优化）
相关: INFO-20251219-026（认知增强系统，推理引擎）
相关: NODE-AI-Agent
触发规则: -
待验证: 使用Z3实现Janus日程冲突检测