2 Preliminaries

A CNF formula F is an AND ($\wedge$) of clauses, where each clause is an OR ($\vee$) of literals, and a literal is a variable or its negation ($\neg$). It is natural to think of F as a set of clauses and each clause as a set of literals. A clause that is a subset of another is called its subclause. The size of F is the number of clauses in F.

Let $\rho$ be a partial assignment to the variables of F. The restricted formula F^$\rho$ is obtained from F by replacing variables in $\rho$ with their assigned values. F is said to be simplified if all clauses with at least one TRUE literal are deleted and all occurrences of FALSE literals are removed from clauses. F|_$\rho$ denotes the result of simplifying the restricted formula F^$\rho$.