Using CSP look-back techniques to solve real-world SAT instances

Abstract

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 real-world problems in planning, scheduling, and circuit diagnosis and synthesis. Our results show that incorporating CSP look-back 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.