Integrating Equivalency Reasoning into Davis-Putnam Procedure

Knowledge Representation and Reasoning

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 17

Boolean Satisfiability

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.