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):
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.