Integrating Equivalency Reasoning into Davis-Putnam Procedure

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.

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.