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

Implement the basic DPLL Algorithm for SAT. Your program should accepts input in the CNF version of the DIMACS format. (This 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 satisfiable, your SAT solver should produce an assignment to all variables such that the formula evaluates to true under this assignment.

If a given formula is unsatisfiable, for now the SAT solver can simply say “false”.

The expected level of sophistication is the simple DPLL solver with unit propagation described in DPLL Algorithm for SAT, it is not required that you implement advanced techniques or very efficient data structures.

You will extend your solver in homework05.