A CNF formula F is an AND () of clauses, where each clause is an OR () of literals, and a literal is a variable or its negation (). 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 be a partial assignment to the variables of F. The restricted formula F is obtained from F by replacing variables in 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| denotes the result of simplifying the restricted formula F.