单元传播

单元传播（UP）或布尔约束传播（BCP）或单字规则（OLR）是一种自动定理证明程序，可以简化一组（通常是命题）条款。

该程序基于单元子句，即由单个字词组成的子句，采用共轭正常形式。因为每个子句都需要被满足，所以我们知道这个字词必须是真的。如果一组子句包含单元子句则其他子句通过应用以下两条规则而被简化。每一个包含l{displaystylel}的子句（除了单元子句本身）都要简化。{displaystylel}的每个子句（单位子句本身除外的每个子句（除了单元子句本身）都被删除（如果该子句满足{displaystylenegl}的每一个子句中，这个字都被删除（如果l{displaystylel}是，子句就满足）。这两条规则的应用导致了一套新的子句，与旧的子句等价。例如，下面这组子句可以通过单元传播来简化，因为它包含单元子句{displaystylendega/veec}包含单元句中字词的否定。包含单元句中字词的否定，这个字词可以从该句中删除。单元句子不被删除；这将使产生的集合不等同于原始集合；如果已经以某种其他形式存储，这个子句可以被删除（见使用部分模型一节）。单元传播的效果可以总结为以下几点。

第二条单元传播规则可以被看作是解析的限制形式，其中两个解析者之一必须始终是一个单元句。对于解析来说，单元传播是一个正确的推理规则，因为它永远不会产生一个没有被旧条款所包含的新条款。单位传播和解析的区别在于。解析是一个完整的反驳程序，而单元传播不是；换句话说，即使一组子句是矛盾的，单元传播也不可能产生不一致；被解析的两个子句在生成的子句被添加到集合中后一般不能被移除；相反，在单元传播中涉及的非单元子句在其简化后被添加到集合中时可以被移除；解析一般不包括单元传播中使用的xxx个规则。包括subsumption的解析计算可以通过subsumption来模拟规则一，通过单元解析步骤来模拟规则二，然后再进行subsumption。单位传播在新的单位条款产生时反复应用，是命题霍恩条款集的完全可满足性算法；如果可满足，它也会为该集产生一个最小模型：见霍恩可满足性。

存在于一个子句集合中的单元子句或者可以从该集合中导出的单元子句可以以部分模型的形式存储（这个部分模型也可能包含其他字词，这取决于应用）。在这种情况下，单元传播是基于部分模型的字面意义进行的，如果单元子句的字面意义在模型中，则被删除。在上面的例子中，单元子句{displaystylea}将被添加到部分模型中。将被添加到部分模型中；然后，条款集的简化将如上所述进行，不同的是，单元条款现在从该集合中删除。在部分模型中的字词有效的假设下，得到的子句集与原来的子句集是等价的。

单位传播的直接实现需要的时间是检查集合总大小的二次方，它被定义为所有子句大小的总和，其中每个子句的大小是它包含的字数。然而，单元传播可以在线性时间内完成，方法是为每个变量存储每个字词所在的子句列表。例如，上面的集合可以通过给每个子句编号来表示。然后为每个变量存储包含该变量或其否定的条款列表。