> For AI agents: the complete documentation index is available at https://shijin.space/llms.txt, the full documentation bundle is available at https://shijin.space/llms-full.txt. # SAT 求解 ## 问题与范围 布尔可满足性问题（Boolean Satisfiability，SAT）询问：能否为公式中的布尔变量赋值，使整个公式为真？找到一组赋值可以回答 SAT；证明所有赋值都不可能满足公式，才能回答 UNSAT。实际求解还可能因资源限制而中止，此时没有得到结论。 本专题讨论以合取范式（CNF）为输入的完备求解，从 DPLL 的搜索与单位传播过渡到 CDCL 的冲突学习，再连接公式变换、搜索控制、结果验证和增量调用。完备算法应在有限时间内返回正确的可满足性结论；这里的保证不意味着运行时间一定短 \[[1, sec. 3.1](https://shijin.space/knowledge/sat/index.md#ref-sat-overview-DarwichePipatsrisawat2021Complete)\]。 理解现代求解器，需要同时掌握搜索和推理的正确性，以及减少传播、冲突分析和整体搜索成本的方法。实际使用还需要说明公式如何表达应用要求，以及返回的模型或证明究竟支持什么结论 \[[2, secs. 4.2–4.4](https://shijin.space/knowledge/sat/index.md#ref-sat-overview-MarquesSilvaLynceMalik2021CDCL)\]。 ## 前置知识与阅读顺序 需要熟悉布尔运算、集合、递归搜索和基本图论；不要求预先了解求解器实现。 1. [SAT 与 DPLL](https://shijin.space/knowledge/sat-dpll/index.md)：明确文字、子句、CNF 和部分赋值，理解 Tseitin 编码与模型投影，再通过 DP/DPLL 的对照理解归结、变量消除、单位传播和分支搜索。 2. [CDCL：从冲突到学习子句](https://shijin.space/knowledge/sat-cdcl/index.md)：记录赋值原因，推导 1-UIP 分析、学习子句最小化与非时间顺序回跳，再把这些步骤对应到传播队列和监视列表。 3. [SAT 预处理、内处理与模型恢复](https://shijin.space/knowledge/sat-preprocessing/index.md)：区分等价与等可满足的公式变换，理解子句吸收、强化、失败文字试探、纯文字和有界变量消除，并从简化后的模型恢复原问题的解。 4. [CDCL 搜索策略：分支、重启与子句管理](https://shijin.space/knowledge/sat-search-strategies/index.md)：通过活跃度、相位保存、重启和子句保留理解搜索控制，区分搜索效果、实现成本与实验结论。 5. [SAT 求解结果的验证](https://shijin.space/knowledge/sat-result-verification/index.md)：检查原公式的模型，手算 RUP 反证与 LRAT 提示，理解公式变换的证明责任和检查器的信任边界。 6. [增量 SAT 与建模实践](https://shijin.space/knowledge/sat-incremental-solving/index.md)：从小型排班问题理解永久约束、临时假设、激活文字和不可满足核心，把求解过程与业务解释连接起来。 第一遍阅读时，先手算传播、回跳、模型恢复、证明检查和排班例子。第二遍再追踪数据结构及接口状态，检查每一步使用的公式、赋值和假设是否一致。MiniSat 的实现说明提供了一个紧凑的参照；较新的求解器可以用来观察这些机制怎样与内处理、证明输出和增量接口组合 \[[3, secs. 3–4](https://shijin.space/knowledge/sat/index.md#ref-sat-overview-EenSorensson2003MiniSat); [4, secs. 2–6](https://shijin.space/knowledge/sat/index.md#ref-sat-overview-BiereEtAl2024Cadical)\]。 ## 基础知识与研究增量 上述六篇构成基础阅读路线，分别覆盖核心算法、实现与变换、搜索控制、结果可信性和应用接口。文中的启发式是可比较的基线，不是对所有实例有效的最优策略；近期实现用于说明机制的演进，其效果仍受版本、配置与实例集合限制。 后续若继续记录研究增量，可以围绕具体贡献展开：搜索策略相对基线改变了什么，公式变换如何保持所需语义，证明生成或检查减少了哪些成本，增量接口支持了哪些原先难以表达的查询。每篇应区分证明、启发式动机与实验观察，并保留可核对的来源。 并行求解、局部搜索、MaxSAT 和 SMT 可以作为延伸方向。并行求解需要额外讨论任务划分与子句共享；局部搜索需要说明能够给出的结果及其限制；MaxSAT 改为优化被满足的约束，SMT 则引入布尔结构之外的理论。它们与本专题有关，但不作为掌握这里的 CNF/CDCL 主线的前置条件。 评价求解效果时，记录实例来源、版本、参数、硬件、资源限制及验证方式。百万变量实例可以被成功求解，并不意味着变量数相近的所有实例都容易；实例结构和编码方式同样影响求解难度 \[[2, secs. 4.1, 4.4.1.1](https://shijin.space/knowledge/sat/index.md#ref-sat-overview-MarquesSilvaLynceMalik2021CDCL)\]。 ## 参考文献 {#references-sat-overview}
1\. Adnan Darwiche and Knot Pipatsrisawat. *Complete algorithms*. Handbook of satisfiability. 2021. [DOI](https://doi.org/10.3233/FAIA200986).
2\. Joao Marques-Silva, Ines Lynce, and Sharad Malik. *Conflict-driven clause learning SAT solvers*. Handbook of satisfiability. 2021. [DOI](https://doi.org/10.3233/FAIA200987).
3\. Niklas Eén and Niklas Sörensson. *An extensible SAT-solver*. Theory and applications of satisfiability testing. 2004. [DOI](https://doi.org/10.1007/978-3-540-24605-3_37).
4\. Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Pollitt. *CaDiCaL 2.0*. Computer aided verification. 2024. [DOI](https://doi.org/10.1007/978-3-031-65627-9_7).
## 配套演示 - [SAT 求解：从 DPLL 到 CDCL · 16:9](https://shijin.space/slides/sat-cdcl/index.html) - [SAT 求解：从 DPLL 到 CDCL · 4:3](https://shijin.space/slides/sat-cdcl/index-4-3.html) - [现代 SAT 求解器：传播、搜索策略与内处理 · 16:9](https://shijin.space/slides/sat-implementation/index.html) - [现代 SAT 求解器：传播、搜索策略与内处理 · 4:3](https://shijin.space/slides/sat-implementation/index-4-3.html) - [使用 SAT：从约束建模到可信结果 · 16:9](https://shijin.space/slides/sat-usage/index.html) - [使用 SAT：从约束建模到可信结果 · 4:3](https://shijin.space/slides/sat-usage/index-4-3.html)