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.

- 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

- 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.

- 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.

- 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.

- 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.

- 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.

General references:

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.

- 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.

- 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.

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:

- 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.

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