Consider the definitions of interpolants in Interpolation for Propositional Logic from lecture06. Prove properties 1,2,3,4 for and .

Build a SAT solver that accepts input in the CNF version of the DIMACS format. (The input file is a formula in conjunctive normal form, where each clause is given on a separate line as a list of indices denoting propositional variables, a negative index indicates a negated propositional variable.)

If a given formula is unsatisfiable, the SAT solver should produce unsatisfiability proof in some format.

If a given formula is satisfiable, the SAT solver should produce an assignment to all variables for which the formula evaluates to true.

You can look at the source code of existing implementations to gain insight into techniques (such as http://sourceforge.net/projects/dpt ) but you are not allowed to copy it, you must write your own implementation.

The expected level of sophistication is a DPLL solver with unit propagation, but you are encouraged to implement additional techniques.

We will run a small competition of implemented solvers.