Sciweavers

Share
AAAI
1997

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

9 years 11 months ago
Using CSP Look-Back Techniques to Solve Real-World SAT Instances
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.
Roberto J. Bayardo Jr., Robert Schrag
Added 01 Nov 2010
Updated 01 Nov 2010
Type Conference
Year 1997
Where AAAI
Authors Roberto J. Bayardo Jr., Robert Schrag
Comments (0)
books