Equivalent literal propagation in the DLL procedure Original Research Article

We propose a simple data structure to represent all equivalent literals such as l1↔l2 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.