Resources

This page contains bibliographic references, and links to online references. We will be augmenting this page as the semester progresses. Due to copyright restrictions, some of the material is in a password-protected directory.

Similar courses and lectures

Shankar et. al, Little engines of proof
Manna and Bradley, Calculus of computation
Barrett, Logic and verification
Tinelli, Decision procedures
Kroening and Strichman, Decision Procedures -- An Algorithmic Point of View

Introduction and quantifier elimination

Barwise, "Introduction to first-order logic," from the Handbook of Mathematical Logic. pdf.
Kreisel and Krivine, "Quantifier elimination," chapter 4 from Elements of Mathematical Logic (Model Theory). pdf.
Harrison, "Decidable Problems," Chapter 5 of a draft of Introduction to Logic and Automated Theorem Proving. pdf.
Abhyankar, "Polynomials and power series, may they forever rule the world!" pdf.

Fast propositional satisfiability solvers

Slides from Ed Clarke's seminar presentation. ppt.
Davis and Putnam, "A Computing Procedure for Quantification Theory." pdf.
Davis, Logemann, and Loveland, "A Machine Program for Theorem-Proving." pdf.
Silva and Sakallah, "GRASP - A New Search Algorithm for Satisfiability." pdf.
Lynce and Marques-Silva, "An overview of backtrack search satisfiability algorithms." pdf.
Lynce and Marques-Silva, "Efficient data structures for backtrack search SAT solvers." pdf.
Moskewicz, Madigan, Zhao, Zhang, and Malik, "Chaff: Engineering an Efficient SAT Solver." pdf.
Eén and Biere, "Effective Preprocessing in SAT through Variable and Clause Elimination." pdf.
Eén and Sörrensen, "An extensible SAT-solver." html. pdf.
Optional exercise: use Mini-SAT to sovle sudoku puzzles: pdf.

DPLL(T)

Ganziger et al., "DPLL(T): fast decision procedures." pdf.
Nieuwenhuis et al., "Abstract DPLL and abstract DPLL modulo theories." pdf.
Nieuwenhuis et al., "Solving SAT and SAT modulo theories: from an abstract David-Putnam-Logemann-Loveland procedure to DPLL(T)." pdf.
Tinelli, "A DPLL-based calculus for ground satisfiability modulo theories." pdf.
Barrett et al., "Splitting on demand in SAT modulo theories." pdf.

Nelson Oppen methods for combining theories

Slides from Tinelli's seminar presentation, "Combination and augmentation method for satisfiability modulo theories." pdf.
A talk by Barrett and Tinelli, "Theory and practice of decision procedures for combinations of theories." pdf.
Slides from Barret's SVC talk, "Satisfiability modulo theories in practice." pdf.
Slides from de Moura's SVC talk, "Developing efficient SMT solvers." pdf.
The SMT-lib initiative. html.

Equality with uninterpreted function symbols

Slides from Constantinos Bartzis's seminar presentation.ppt.
Nelson and Oppen, "Fast decision procedures based on congruence closure." Portal link.
Niewenhuis and Oliveras, "Fast congruence closure and extensions." pdf.

Linear arithmetic (the linear theory of the reals)

General references:

"Linear programming" in Wikipedia. html.
The Kroening and Strichman site above. html.

The Fourier-Motzkin procedure:

Excerpt from Apt, Principles of Constraint Programming. pdf.

The Simplex method:

Excerpt from Papadimitriou and Steiglitz, Combinatorial Optimization: Algorithms and complexity. pdf.
Gale, "Linear programming and the simplex method." html.
"The simplex method" in Wikipedia. html.
Cottle et al., biography of George Dantzig: html.

The test-point method:

Weispfenning, "The complexity of linear problems in fields." pdf.

Integer arithmetic (aka Presburger arithmetic, the linear theory of the integers)

Slides from Constantinos Bartzis's presentation, ppt. These are based on lectures by Michael Norrish, which can be found here: html.
A simple algorithm can be found in Kreisel and Krivine.
Cooper, "Theorem proving in arithmetic without multiplication." pdf.
A description of Cooper's algorithm can also be in the chapter from Harrison's book.
See also Pugh's paper on the omega test under "mixed integer linear arithmetic."
Boudet and Comon, "Diophantine equations, Presburger arithmetic and finite automata." html.

Mixed integer linear arithmetic

Pugh, "The Omega test: a fast and practical integer programming algorithm for mixed integer-linear arithmetic". pdf.

"Online" versions, suitable for DPLL(T):

Berezin, Ganesh, and Dill, "An online proof-producing decision procedure for mixed-integer linear arithmetic." ps. pdf.
Berezin, Ganesh, and Dill, expanded tech-report version of the preceeding paper. ps. pdf.
Dutertre and de Moura, "A fast linear-arithmetic solver for DPLL(T)." html.
Dutertre and de Moura, "Integrating simplex with DPLL(T)" (an expanded version of the preceding paper). html.

Real closed fields

The Kreisel-Krivine proof:

See the chapter from Kreisel and Krivine's textbook, above.
Excerpt from Engeler, Foundations of Mathematics: Questions of Analysis, Geometry and Algorithmics. pdf.

The Cohen/Hormander proof:

Cohen "Decision procedures for real and p-adic fields." pdf.
McLaughlin and Harrison, "A proof-producing decision procedure for real arithmetic." pdf.
See the the chapter from Harrison's book, above.

Cylindrical Algebraic Decomposition:

Arnon et al., "Cylindrical algebraic decomposition I: the basic algorithm." pdf.
Arnon et al., "Cylindrical algebraic decomposition II: an adjacency algorithm for the plane." pdf.
Basu, Costa, Roy, Algorithms in Real Algebraic Geometry. html.
See also Mishra, B., Algorithmic Algebra. Excerpt on resultants and subresultants: pdf. Errata: html.

Sums of squares, and the universal fragment:

Harrison talk, "Sums of squares for real closed fields" (CMU, March 19). pdf.

Heuristic methods for real inequalities:

Avigad and Friedman, "Combining decision procedures for the reals." html.
A related talk. pdf.

Theory of bit vectors

Barrett, Dill, and Levitt. "A decision procedure for bit-vector arithmetic." portal.
Bryant et al., "Deciding Bit-vector arithmetic with abstraction." pdf.
Möller, "Solving bit-vector equations." html.
Ganesh, Berezin, Dill, "A decision procedure for fixed-width bit-vectors (technical report)." ps.

Computational complexity

Some information on complexity bounds for linear and integer arithmetic can be found in the following review by Charles Rackoff. html.