Unit Clause

定义 (Definition)

unit clause（单子句/单位子句）：在命题逻辑的合取范式（CNF）中，只包含一个文字（literal）的子句，例如 (p) 或 (¬q)。它在 SAT 求解中很重要，因为可直接触发单位传播（unit propagation）。

发音 (Pronunciation, IPA)

/ˈjuːnɪt klɔːz/

例句 (Examples)

A unit clause like (p) forces p to be true.
像 (p) 这样的单位子句会迫使 p 为真。

During SAT solving, the algorithm repeatedly applies unit clause propagation to simplify the CNF, sometimes leading quickly to a contradiction.
在 SAT 求解过程中，算法会反复进行单位子句传播来简化 CNF，有时会很快导向矛盾（从而判定不可满足）。

词源 (Etymology)

unit 表示“单个的、一个单位的”，clause 在逻辑/语法中指“子句/从句”，组合起来字面义就是“只含一个元素的子句”。该术语主要在计算机科学与数理逻辑（尤其是 SAT/自动推理）语境中固定使用。

相关词 (Related Words)

• Clause
• Literal
• CNF
• SAT
• Unit Propagation
• Resolution
• Horn Clause
• DPLL

文学与著作中的用例 (Notable Works)

• Handbook of Satisfiability（章节中讨论 unit clause 与 unit propagation，是 SAT 领域权威参考书）
• Artificial Intelligence: A Modern Approach（在逻辑推理与可满足性相关内容中提到单位子句/传播思想）
• Logic for Computer Science: Foundations of Automatic Theorem Proving（自动定理证明与归结法语境下常出现 unit clause）