The Theory of Computation

Bernard M.E. Moret

Addison-Wesley-Longman, 1998


Detailed Solutions

Chapter 7, Problem 7.39




We want to identify a variable, x, such that the clauses imply (x -> not x) and (not x -> x), a contradiction; in fact, we will prove that a set of 2-CNF clauses is a contradiction if and only if such a variable exists. Since -> is transitive, the implications may be through a chain,

(x -> y1)(not y1 -> y2) ... (not yk -> not x)

and

(not x -> z1)(not z1 -> z2) ... (not zl -> x)

Recalling that (a-> b) is equivalent to ((not a)+b), we then claim:

A Boolean formula in 2-CNF is not satisfiable if and only if there exist two subsets of clauses {(x+x1)(not x1+x2)...(not xk +x)} and {(not x+xk+1)(not xk+1+xk+2)...(not xn+ not x)}

The if part is trivial. If we can prove the only if part, then it is obvious that the problem is in NL, since we can guess the series of clauses and then verify their existence in the original expression.

To prove the only if part, we proceed by induction on the number of clauses. The basis is trivial. Suppose that the theorem holds true for all instances of n and fewer clauses. The formula is not satisfiable if and only if neither of its restrictions to x=true and x=false is satisfiable either. But each restriction can be simplified down to a 2-CNF formula with fewer clauses: each clause in which x appears either has a literal set true -- in which case it can be dropped -- or a literal set to false, in which case we set the other one to true, continuing until we get a contradiction (a clause wit both literals set to true) or until we are left only with clauses of 2 as-yet-undefined literals. In the latter case, the resulting 2-CNF must also be unsatisfiable, so that the inductive hypothesis applies and we get the desired collection of clauses. In the earlier case, another induction proof (this time trivial) on the number of clauses involved in forcing other literals shows that we have the desired pattern of clauses. Hence our proof is complete.

Now, to show that the problem is complete, we transform Digraph Reachability to it. Each vertex, i, will become a variable, xi; for each arc (i,j), we set up the clauses (not xi+xj). Finally, we add three clauses: (not xn+not x1), (x1+xn+1), and (x1+not xn+1). The last two clauses can only be satisfied by setting x1=true; using this in the previous clause forces xn=false. But then, if vertex n is reachable from vertex 1, we have the implication
x1 implies xn
a contradiction. The converse is equally easy.