Integrating equivalence reasoning into davis-putnam procedure

Equivalency clauses (Xors or modulo 2 arithmetics) repre-sent a common structure in the SAT-encoding of many hard real-world problems and constitute a major obstacle to Davis-Putnam (DP) procedure. We propose a special look-ahead technique called equivalency reasoning to overcome the ob-stacle and report on the performance of an equivalency rea-soning enhanced DP procedure on SAT instances containing equivalency clauses derived from problems in parity learn-ing, cryptographic key search and model checking. Our results show that integrating equivalency reasoning renders easy many problems which were beyond DP’s reach. We also compare equivalency reasoning with general CSP look-back techniques on equivalency clauses