SAT 求解#

#问题与范围

布尔可满足性问题（Boolean Satisfiability，SAT）询问：能否为公式中的布尔变量赋值，使整个公式为真？找到一组赋值可以回答 SAT；证明所有赋值都不可能满足公式，才能回答 UNSAT。实际求解还可能因资源限制而中止，此时没有得到结论。

本专题讨论以合取范式（CNF）为输入的完备求解，从 DPLL 的搜索与单位传播过渡到 CDCL 的冲突学习，再连接公式变换、搜索控制、结果验证和增量调用。完备算法应在有限时间内返回正确的可满足性结论；这里的保证不意味着运行时间一定短 [1, sec. 3.1]。

理解现代求解器，需要同时掌握搜索和推理的正确性，以及减少传播、冲突分析和整体搜索成本的方法。实际使用还需要说明公式如何表达应用要求，以及返回的模型或证明究竟支持什么结论 [2, secs. 4.2–4.4]。

#前置知识与阅读顺序

需要熟悉布尔运算、集合、递归搜索和基本图论；不要求预先了解求解器实现。

1. SAT 与 DPLL：明确文字、子句、CNF 和部分赋值，理解 Tseitin 编码与模型投影，再通过 DP/DPLL 的对照理解归结、变量消除、单位传播和分支搜索。
2. CDCL：从冲突到学习子句：记录赋值原因，推导 1-UIP 分析、学习子句最小化与非时间顺序回跳，再把这些步骤对应到传播队列和监视列表。
3. SAT 预处理、内处理与模型恢复：区分等价与等可满足的公式变换，理解子句吸收、强化、失败文字试探、纯文字和有界变量消除，并从简化后的模型恢复原问题的解。
4. CDCL 搜索策略：分支、重启与子句管理：通过活跃度、相位保存、重启和子句保留理解搜索控制，区分搜索效果、实现成本与实验结论。
5. SAT 求解结果的验证：检查原公式的模型，手算 RUP 反证与 LRAT 提示，理解公式变换的证明责任和检查器的信任边界。
6. 增量 SAT 与建模实践：从小型排班问题理解永久约束、临时假设、激活文字和不可满足核心，把求解过程与业务解释连接起来。

第一遍阅读时，先手算传播、回跳、模型恢复、证明检查和排班例子。第二遍再追踪数据结构及接口状态，检查每一步使用的公式、赋值和假设是否一致。MiniSat 的实现说明提供了一个紧凑的参照；较新的求解器可以用来观察这些机制怎样与内处理、证明输出和增量接口组合 [3, secs. 3–4; 4, secs. 2–6]。

#基础知识与研究增量

上述六篇构成基础阅读路线，分别覆盖核心算法、实现与变换、搜索控制、结果可信性和应用接口。文中的启发式是可比较的基线，不是对所有实例有效的最优策略；近期实现用于说明机制的演进，其效果仍受版本、配置与实例集合限制。

后续若继续记录研究增量，可以围绕具体贡献展开：搜索策略相对基线改变了什么，公式变换如何保持所需语义，证明生成或检查减少了哪些成本，增量接口支持了哪些原先难以表达的查询。每篇应区分证明、启发式动机与实验观察，并保留可核对的来源。

并行求解、局部搜索、MaxSAT 和 SMT 可以作为延伸方向。并行求解需要额外讨论任务划分与子句共享；局部搜索需要说明能够给出的结果及其限制；MaxSAT 改为优化被满足的约束，SMT 则引入布尔结构之外的理论。它们与本专题有关，但不作为掌握这里的 CNF/CDCL 主线的前置条件。

评价求解效果时，记录实例来源、版本、参数、硬件、资源限制及验证方式。百万变量实例可以被成功求解，并不意味着变量数相近的所有实例都容易；实例结构和编码方式同样影响求解难度 [2, secs. 4.1, 4.4.1.1]。

#参考文献