Larry Paulson's Project Suggestions

A High-Performance Satisfiability Checker

Modern Boolean satisfiability checkers are fast enough to solve problems in tens of thousands of variables. This performance is the product of numerous refinements to the Davis-Putnam-Logeman-Loveland (DPLL) procedure. Early work on heuristics to minimize the search space has been eclipsed by an emphasis on low-level concerns, such as minimizing the number of cache misses. Data structures, e.g. to represent clauses, are carefully designed to minimize memory references in the most heavily-used algorithms.

A survey paper [1] outlines the basic DPLL satisfiability method and describes some of the most important refinements, with references to many other papers where you can find more details. The project is to implement DPLL and its most important refinements and to compare your system's performance with that of a leading one, such as Chaff. If you enjoyed Logic and Proof but also enjoy writing fast code in C, this project may be for you.

  1. Lintao Zhang and Sharad Malik, The Quest for Efficient Boolean Satisfiability Solvers
    In: A. Voronkov (Ed.), Automated Deduction — CADE-18 (Springer LNAI 2392, 2002), pages 295–313.

Also see the Chaff group's other publications.

A Decision Procedure for Quantified Formulas over the Real Numbers

Gödel's incompleteness theorem tells us that the theory of the integers with addition and multiplication is undecidable, but the situation is quite different for the reals. Quantifiers can be eliminated from any formula about the reals that concerns only addition and multiplication. In particular, if the formula contains no free variables, it can be reduced to true or false.

A simple example of quantifier elimination is to state precise conditions for the existence of a solution x to the quadratic equation ax2+b+c = 0. Here, an existential quantification over x can be replaced by conditions on a, b and c.

Tarski's original decision procedure for the reals is too inefficient to handle even small examples. The most efficient procedure, Collin's cylindrical algebraic decomposition, is probably too difficult to undertake as a student project; this procedure would have to be implemented within a computer algebra system. However, a procedure credited to Paul Cohen is straightforward to implement and efficient enough to manage some interesting examples.

John Harrison has described this procedure in an unpublished manuscript, including source code listings written in Objective Caml. More code is available from his website. So, building a basic quantifier elimination procedure would be an easy first milestone of the project. (Needless to say, Caml should not be used!) A worthwhile project should include extensions to the basic procedure. Here are some ideas for such extensions:

Last revised: 12 January, 2012
Lawrence C. PaulsonComputer LaboratoryUniversity of Cambridge