Unit-Propagation

释义 Definition

单元传播：在布尔可满足性（SAT）与命题逻辑求解中，一旦某个子句（clause）只剩下一个未确定的文字（即“单元子句”，unit clause），就强制该文字取能满足该子句的真值，并将这一赋值的影响继续向其他子句扩散，从而推导出更多必然赋值或发现矛盾。
（在现代 CDCL SAT 求解器中，unit propagation 是最核心、最频繁执行的推理步骤之一。）

发音 Pronunciation (IPA)

/ˈjuːnɪt ˌprɒpəˈɡeɪʃən/

例句 Examples

Unit propagation quickly forces (x) to be true.
单元传播会很快迫使 (x) 取真。

After each decision, the solver runs unit propagation to derive implied assignments and detect conflicts early.
每次做出一个决策赋值后，求解器都会运行单元传播来推出蕴含赋值，并尽早检测冲突。

词源 Etymology

unit 在这里指“单元子句”（只含一个未满足/未确定文字的子句）；propagation 表示“传播/扩散”。合起来就是“由单元子句触发的强制赋值，并将其影响不断传播”的过程。该术语广泛出现于 DPLL/CDCL 等 SAT 求解算法传统中。

相关词 Related Words

• Boolean Satisfiability
• Clause
• Literal
• Unit Clause
• DPLL
• CDCL
• Constraint Propagation
• Resolution
• Implication Graph

文学与著作中的用例 Literary Works

• Handbook of Satisfiability（Biere, Heule, van Maaren, Walsh 编）：系统讨论 unit propagation 在现代 SAT 求解中的地位与实现细节。
• “A Fast and Effective Heuristic for SAT Solvers”（Moskewicz et al., Chaff）：描述高效 SAT 求解器中以 unit propagation 为核心的工程优化。
• “The Davis-Putnam Procedure for Theorem Proving”（Davis & Putnam）：早期奠基性工作之一，为后续以单元推理为关键步骤的程序体系铺路。