Practical Decision Procedures
This is the home page for a seminar that was taught by Jeremy Avigad (avigad@cmu.edu) and Ed Clarke (emc+@cs.cmu.edu) at Carnegie Mellon University in the Spring of 2007. The seminar was cross-listed in Philosophy (80-813) and Computer Science (15-829), and met on Fridays, from 1:30-2:50, in Wean 4615A.
In recent years, fast propositional satisfiability solvers have been developed that can often handle formulas in CNF with hundreds of thousands of variables and millions of clauses. These have made it possible to apply classical decision procedures to domains where, previously, they were applicable only in theory. As a result, we can now reason effectively in the presence of increasingly complex systems of arithmetic and algebraic constraints.
This course will survey the fundamental methods behind these core decision procedures. Topics will include Groebner bases, decision procedures for real and integer linear arithmetic, and decision procedures for real closed fields. We will also cover Nelson-Oppen methods, which provide ways of combining decision procedures for languages with restricted overlap.
This is a six-unit seminar, but students can earn an additional six units by completing a suitable final project. Auditors and visitors are welcome.
There a resources page, with links and references.
There is a course overview, that provides an overview of the lectures and topics we covered.
In the seminar, we discussed fast satisfiability solvers, satisfiability modulo theories, the DPLL(T) framework, and Nelson-Oppen combination methods; and decision procedures for equality with uninterpreted function symbols, linear arithmetic, integer arithmetic, and real closed fields. Two topics we did not cover are Groebner bases and decision procedures for the theory of bit-vectors.