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

Introduction and quantifier elimination

Fast propositional satisfiability solvers


Nelson Oppen methods for combining theories

Equality with uninterpreted function symbols

Linear arithmetic (the linear theory of the reals)

General references:

The Fourier-Motzkin procedure:

The Simplex method:

The test-point method:

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

Mixed integer linear arithmetic

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

Real closed fields

The Kreisel-Krivine proof:

The Cohen/Hormander proof:

Cylindrical Algebraic Decomposition:

Sums of squares, and the universal fragment:

Heuristic methods for real inequalities:

Theory of bit vectors

Computational complexity

Related topics and materials