Chu Min Li, Univ. de Picardie Jules Verne
Equivalency clauses (Xors or modulo 2 arithmetics) represent a common structure in the SAT-encoding of many hard real-world problems and constitute a major obstacle to Davis-Putnam (DP) procedure. We report on the performance of an equivalency reasoning enhanced DP procedure on SAT instances containing equivalency clauses derived from problems in parity learning, 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.