clause learning：子句学习；常指在布尔可满足性（SAT）求解等领域中的一种技术——在搜索过程中从冲突中总结并“学习”新的约束子句（通常是子句形式），以避免重复走回头路、加速求解。最常见语境是 CDCL（Conflict-Driven Clause Learning，冲突驱动子句学习）。
/klɔːz ˈlɜːrnɪŋ/
Clause learning helps the solver avoid repeating the same mistakes.
子句学习能帮助求解器避免重复犯同样的错误。
In modern SAT solvers, conflict-driven clause learning records new clauses from conflicts, guiding backtracking and dramatically improving performance on hard instances.
在现代 SAT 求解器中，冲突驱动子句学习会从冲突中记录新的子句，引导回溯，并显著提升在困难实例上的性能。
clause 源自拉丁语 clausula（“句子、条款、结尾”），与 claudere（“关闭”）同源，后来在语法与法律语境中指“从句/条款”，在逻辑与计算机科学中进一步发展为“子句”（由若干文字组成的析取）。
learning 来自古英语 leornian（“学习、获得知识”）。组合成 clause learning 时，含义转为“学习（并添加）新的子句/约束”。
Select Language