Boolean Satisfiability Information Page
I'm very interested in Boolean satisfiability and unsatisfiability at
the moment. Here are some interesting papers I've run across.
- 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.
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.
- Slides from a talk by Bart Selman on AI and Physics.
Created by Michael Littman: Wed Oct 15 11:40:38 EDT 1997
- 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