Using CSP Look-Back Techniques to Solve Real-World SAT Instances

Roberto J. Bayardo Jr., Robert C. Schrag

We report on the performance of an enhanced version of the "Davis-Putnam" (DP) proof procedure for propositional satisfiability (SAT) on large instances derived from realworld problems in planning, scheduling, and circuit diagnosis and synthesis. Our results show that incorporating CSP lookback techniques -- especially the relatively new technique of relevance-bounded learning -- renders easy many problems which otherwise are beyond DP’s reach. Frequently they make DP, a systematic algorithm, perform as well or better than stochastic SAT algorithms such as GSAT or WSAT. We recommend that such techniques be included as options in implementations of DP, just as they are in systematic algorithms for the more general constraint satisfaction problem.


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.