CDCL

释义 Definition

CDCL（Conflict-Driven Clause Learning）指“冲突驱动子句学习”，是一类现代 SAT（布尔可满足性）求解器的核心算法框架：在搜索过程中一旦遇到矛盾（冲突），就分析冲突原因并学习（加入）新的子句，从而避免重复走入同类死胡同，提高求解效率。（也常被用来泛指“采用 CDCL 的 SAT 求解器”。）

发音 Pronunciation

/ˌsiːdiːsiːˈɛl/

例句 Examples

CDCL solvers can handle many large SAT instances efficiently.
CDCL 求解器可以高效处理许多大型 SAT 实例。

By learning a clause from each conflict and using non-chronological backtracking, CDCL often prunes huge parts of the search space.
通过从每次冲突中学习子句并采用非按时间顺序的回溯，CDCL 往往能剪枝掉搜索空间中极其庞大的部分。

词源 Etymology

CDCL 是由四个英文词首字母组成的缩写：Conflict（冲突）+ Driven（驱动的）+ Clause（子句）+ Learning（学习）。该术语主要在计算机科学中讨论 SAT 求解器时使用，可视为对经典 DPLL 框架加入“冲突分析 + 子句学习”等机制后的现代化发展称呼。

相关词 Related Words

• SAT
• Solver
• Clause
• Conflict
• Backtracking
• Backjumping
• Unit Propagation
• Resolution
• Heuristic
• DPLL

文学与著作 Literary Works

• Marques-Silva & Sakallah (1999), GRASP: A Search Algorithm for Propositional Satisfiability（早期系统化呈现冲突分析/学习思想的 SAT 求解器论文）
• Moskewicz et al. (2001), Chaff: Engineering an Efficient SAT Solver（以工程化实现推动 CDCL 系方法普及的经典论文）
• Eén & Sörensson (2003), *An Extensible SAT-solver (MiniSat)*（MiniSat 相关论文，CDCL 求解器的代表性工作）
• Biere, Heule, van Maaren & Walsh (eds.), Handbook of Satisfiability（综述 SAT 与 CDCL 等关键技术的权威参考书）