To get started on our SAT solver bakeoff, here are some satisfiability problems generated from the AI
planning system BlackBox, and and a program by Valeria to generate SAT
problems from the 15 puzzle. The source code and executable for
Valeria's program is also there. and a few
sat solvers that I've downloaded (executables are for linux).
Others are available on the SATLIB page (see below).
I removed some garbage in the "prob-*" files in SATPROBLEMS (4/24/01, 5:30PM)
The lecture schedule should not be trusted unless the lectures have already occured. But here is a rough idea.
Lecture 1 (4/4) Getting organized.
Lecture 2 (4/9) Programs for the SAT problem
Here is a page with a lot of benchmark results.
Lecture 3 (4/11) More on GRASP. Heuristics for unit propagation.
Stochastic methods.
Lecture 4 (4/16) Matthew Moskewicz will speak about his SAT program, Chaff.
Reading: Chaff: Engineering an Efficient SAT Solver
Matthew W Moskewicz, Conor F. Madigan, Sharad Malik, Design Automation Conference 2001.
Lecture 5 (4/18) More SAT.
Lecture 6 (4/23)
Quantifier-free FOL: Cooperating Decision Procedures (Nelson/Oppen and beyond).
Clark Barrett. Read:
Cesare Tinelli and Mehdi Harandi A New Correctness Proof of the
Nelson-Oppen Combination Procedure. Proceedings of the
1st International Workshop ``Frontiers of Combining
Systems'' (FroCoS'96), Munich, Germany, March 26-29,
1996.
Lecture 7 (4/25) Quantifier-free FOL: (Shostak's approach).
Clark Barrett.
(Belatedly) The reading is an unpublished paper by Clark
presenting Shostak's scheme for combining decision procedures in
a new way.
Lecture 8 (4/30) Clark finishes up.
Lecture 9 (5/2) Congruence closure (Downey, Sethi, Tarjan).
[sections 1,2,4,5 are relevant. A lot of the discussion is
devoted to the "fast acyclic case," which appears not to
be useful to us.]
Aaron Stump "Small domain instantiations" (reduction to SAT)
Reading:
"Deciding Equality
Formulas by Small Domain Instantiations", by Pnueli, Rodeh,
Shtrichman, and Siegel, from CAV'99
Lecture 10 (5/7) Probably more Aaron.
Lecture 11 (5/9) Presburger arithmetic. (Vijay Ganesh)
Quantifier elimination, Cooper's method
Lecture 12 (5/14) Linear arithmetic on the reals (Shaz Qadeer)
Lecture 13 (5/16) Presburger arithmetic
Reading: Omega tool .
Supplementary reading (not in lecture) comparing Presburger procedures
Lecture 14 (5/21) Mona (Yannick Moy)
Here is the paper.
You may also want to look over the Mona
web site.
Here are some other Presburger procedures:
Reading: GRASP: A Search Algorithm for Propositional Satisfiability,
Joao P. Parques-Silva and Karem A Sakallah, IEEE Trans. on Computers, Vol 48, No. 5, May 1999.
Handed out physically.
Satlib has a wealth of information: solvers, benchmarks,
results on benchmarks, an annotated bibliography, etc.
Readings: Heuristics Based on Unit Propagation for Satisfiability Problems
by Chu Min Li and Anbulagan,
in proceedings of 15th International Joint Conference on Artificial Interlligence (IJCAI'97), Morgan
Kaufmann Publishers, ISBN 1-55860-480-4, Page 366-371, Japan, 1997.
Toward an understanding of hill-climbing Procedures for SAT
Extended version of a paper in AAAI-93.
Binaries for Chaff are available
if you would like to give it a try.
Martin Luther King day (5/28)
Lecture 16 (5/30) Generalized Nelson-Oppen combination of overlapping theories
(Calogero Zarba).
Reading:
[Rin96b] Christophe Ringeissen. Cooperation of decision procedures for the
satisfiability problem. In Franz Baader and Klaus U. Schulz,
editors, Frontiers of Combining Systems (FroCoS '96), volume 3 of
Applied Logic Series, pages 121-140, Kluwer Academic Publishers,
1996.
The most recent report on the topic is:
[TR01] Cesare Tinelli and Christophe Ringeissen. Unions of non-disjoint
theories and combinations of satisfiability procedures. Technical
Report 01-02, Department of Computer Science, University of Iowa,
2001
[I'll be in St. Louis, unfortunately].
Lecture 17 (6/4) Quantifier instantiation in Simplify (Shaz Qadeer).
Lecture 18 (6/6) TBA.