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.