Unsatisfiable Cnf Instances

Unsatisfiable CNF instances
Consider the unsatisfiable CNF formula represented by the DIMACS file in Figure 18.4: An important theorem pertaining to unsatisfiable

CNF formulas is the following:
Theorem 18.1. In any unsatisfiable CNF formula, for any assignment, there will be one clause with all its variables false and another with all its variables true.
Proof: We can prove this fact by contradiction, as follows. Suppose Fmla is an unsatisfiable CNF formula and there is an assignment σ under which one of the following cases arise (both violating the ‘one clause with all its variables false and another with all its variables true’ requirement):

• There are no clauses with all its literals assuming value true. In this case, we can complement the assignment σ, thus achieving a situation where no clause will have all false values.
• There are no clauses with all its literals assuming value false. In this case, Fmla is satisfiable.

If we feed the file in Figure 18.4 to a SAT solver, it will conclude that the formula is indeed unsatisfiable. In modern SAT solvers, it is possible to find out the root cause for unsatisfiability. In particular, if the clauses of Figure 18.4 were embedded amidst many other clauses, upon finding the system to be unsatisfiable, a modern SAT solving framework is capable of extracting the clauses of Figure 18.4 as the root cause.