Equivalent literal propagation in the DLL procedure
Equivalent literal propagation in the DLL procedure
复制标题
DOI：
10.1016/s0166-218x(02)00407-9
复制
发表时间：
2003-08-15
影响因子：
1.1
通讯作者：
Li, CM
中科院分区：
文献类型：
--
作者：
Li, CM
我们提出了一种简单的数据结构来表示CNF公式F中所有的等价文字，如l（1）l（2），并实现了一种特殊的前瞻技术，称为等价推理，传播这些等价文字在F中，以获得其他等价文字和简化F。等价文字传播弥补了单位传播在等价文字上的无效性，使许多包含通常的CNF子句和所谓的等价子句（Ex-OR或模2算术）的SAT问题变得容易。我们的方法也比较一般CSP回看这些问题的技术。(C)2003 Elsevier B. V.保留所有权利。
We propose a simple data structure to represent all equivalent literals such as l(1) l(2) in a CNF formula F, and implement a special look-ahead technique, called equivalency reasoning, to propagate these equivalent literals in F in order to get other equivalent literals and to simplify F. Equivalent literal propagation remedies the ineffectiveness of unit propagation on equivalent literals and makes easy many SAT problems containing both usual CNF clauses and the so-called equivalency clauses (Ex-OR or modulo 2 arithmetics). Our approach is also compared with general CSP look-back techniques on these problems. (C) 2003 Elsevier B.V. All rights reserved.