Boolean Satisfiability Information Page

Systematic Methods

• Crawford: postscript
• As fast as walksat for some real problems? compressed postscript
• Excellent review by Douglas Edwards (Berkeley): html
  
  Thoughts: Amazing summary. Talks about using lookahead to decide which variables to flip. This seems like an obvious candidate for Justin Boyan's STAGE. Edwards argues that ``extended DP'' is needed for UNSAT because DPLL is best-case exponential on some important problems and WSAT can't do UNSAT at all. The east-hardest-hard pattern appears to be algorithm independent. There is a class of problems for which DPLL beats GSAT. Cites Urquhart 1987 is a source of information about exponential lower bounds for DPLL. Mentions pigeonhole and xor as two problems hard for DPLL that probably are important in practice. Mentions that insights from dynamic programming could help.
• SATO: an optimized version of DP.
• Directional Resolution: The Davis-Putnam Procedure, Revisited, Rina Dechter and Irina Rish, in Proceedings of KR-94, 1994. An extended version is also available.
  
  Thoughts and comments (ML 10/17/97): Attempts to revive the original DP algorithm that uses resolution instead of splitting. For uniform random propositional theories, splitting is much better. But for some chains, resolution beats splitting. Seems to imply that the result of resolution can be used to generate all models (i.e., all satisfying assignments). If this were true, it might be possible to use this to count models as well. It's not obvious from the model-generation algorithm (Theorem 1), however. Describes induced width of the interaction graph as a way to bound the running time. Chains have small induced width, so this algorithms runs well for chains. Diversity is a more careful measure that takes into consideration the number of positive and negative instances of each variable. Some other tractibility results: theories with zero diversity, 2-CNF. From what I can tell, the splitting rule is efficient for these as well (actually, probably more so). And the random chains they give could be solved incredibly easily by the weak link heuristic that we've thought about. Mentions backjumping, which seems better still (what is it?) In references: Crawford and Auton: DP heuristic, Bertele and Brioshi: connection to dynamic programming, Dechter: backjumping, Goldberg, Purdom, and Brown: Average-time analysis of DP, Selman, Levesque, Mitchell: GSAT.

Random Search

• GSAT, WALKSAT.

Random Instances

• Slides from a talk by Bart Selman on AI and Physics.

Planning

• Kautz paper on representing planning problems using satisfiability: postscript, another one
• Kautz and Selman's actual SATPLAN algorithm.
• UW paper on sizes of formulas from planning problems: postscript