Read a file in DIMACS CNF format. It will contain:

• possibly comment lines starting with c
• a line defining the problem: p cnf followed by the number V of propositions (represented as numbers from 1 to V) and the number C of clauses
• the clauses, each given as a whitespace-separated list of numbers from -V to V (negated or positive variables) ending with a 0.

For each variable v from 1 to V:

• Find the set of clauses where it appears positively (v) or negatively (-v). If a variable appears both ways in one clause, that clause can be removed, being true. Assume you have found p clauses with v and n clauses with -v .
• If there are none, do nothing. If p is 0, set v to false, and delete the n clauses. If n is 0, set v to true, and delete the p clauses.
• Otherwise, form the p*n clauses obtained by joining a clause with v and a clause with -v (taking all numbers, except v and -v). Add these clauses to the clause list. If any of them is empty, stop and report the formula is unsatisfiable. Else, delete the original p+n clauses with v and -v . (Now, there is no more v).