Overview

Meeting 1, January 19

Jeremy sketched the logical background needed for the course, provided an overview of the types of decision procedures we are interested in, and discussed quantifier elimination methods in particular. Barwise's article provides a nice overview of first-order logic.

Meeting 2, January 26

Jeremy described some of the most important quantifier-elimination procedures, including the theory of the reals as an additive group (= "linear arithmetic"), the theory of the integers as an additive group (="Presburger arithmetic"), the theory of the complex numbers as a field (= "algebraically closed fields of characteristic zero"), and the theory of the reals as an ordered field (= "theory of real closed fields").

Most of the material is covered in Kresiel and Krivine. For linear arithmetic, the Fourier-Motzkin procedure is described in Apt's book; but this is essentially the same as the treatment of dense linear orderings in Kreisel and Krivine. More algorithmic treatments can be found in Harrison's textbook.

Meeting 3, February 2

Ed discussed the ideas behind the recent fast propositional SAT solvers, and GRASP in particular. Slides are on the resources page.

The first two references on the resources page are of historical interest. The most important reference is the paper on GRASP; the other two articles by Silva provide some helpful background. An optional exercise, using MiniSAT to solve sudoku puzzles, is also posted on the resources page.

Meeting 4, February 9

Ed presented an abstract formulation of DPLL, based on the paper Nieuwenhuis et al., "Solving SAT and SAT modulo theories: from an abstract David-Putnam-Logemann-Loveland procedure to DPLL(T)."

Meeting 5, February 16

Constantinos Bartzis presented the quantifier-free theory of equality with uninterpreted function symbols, Nelson and Oppen's classic congruence closure algorithm, and a more recent version, suited to DPLL(T), due to Niewenhuis and Oliveras. Slides and links to the two papers are on the resources page.

Meeting 6, February 23

Ed finished his presentation of the abstract formulation of DPLL(T), and an "API" for the T-solver.

Meeting 7, March 2

Jeremy presented the simplex method, sticking closely to the excerpt from Papadimitriou and Steiglitz's book (under "simplex method" on the resources page), and the article by Gale.

SVC lecture, March 19

John Harrison, Intel Corporation, "Sum-of-Squares Approaches To The Universal Theory Of Real-Closed Fields." Slides from this talk, and another talk delivered at Pitt a few days later, are posted on the resources page.

Meeting 8, March 23

Contantinos discussed various decision methods for integer (Presburger) arithmetic: Fourier-Motzkin / the omega test, Cooper's algorithm, and automata-theoretic techniques.

Meeting 9, March 30

Jeremy discussed "online" methods for mixed integer linear arithmetic, based on the papers by Berezin, Ganesh, and Dill and Dutertre and de Moura on the resources page. Both are available on the resources page, under "mixed integer linear arithmetic," followed by expanded versions (as technical reports).

Meeting 10, April 6

Jeremy began discussing the theory of real closed fields, based on the excerpt from Engeler's book, on the resources page.

Meeting 11, April 13

Cesar Tinelli, University of Iowa, "Combination and Augmentation Methods for Satisfiability Modulo Theories."

SVC lecture, April 16

Clark Barrett, New York University, "Satisfiability Modulo Theories in Practice."

Meeting 12, April 20

Sean McLaughlin presented the Cohen/Hormander decision procedure for real closed fields, and discussed a proof-producing implementation he developed with John Harrison.

Meeting 13, April 27

Ed presented an overview of cylindrical algebraic decomposition.

Meeting 14, March 4

Jeremy and Ed discussed some of the details behind CAD, including resultants, subresultants, and root isolation.

SVC lecture, May 7

Leonardo de Moura, Microsoft Corporation, "Developing Efficient SMT Solvers."

Meeting 15, March 11

Jeremy discussed the theory behind Nelson-Oppen methods for combining decision procedures, and the problem of verifying real inequalities in ordinary mathematical proofs. Links to his paper with Friedman and associated slides can be found on the resources page.