420 CHAPTER 6 Graph Theory
- Recall the discussion of satisfiability in propositional logic from Chapter 2 in Section
2.3.1. One of the cases in which satisfiability is easy to check is the case of 2-CNF
formulas-conjunctions such as
0 = (-p V -q) A (-'p V q) A (p V -q) A (p V q)
X = (-'p V q) A (p V -q) A (p V q)
where each clause has just two literals. That is, each clause is of the form X1 V X 2 ,
where each )q is either a proposition letter xi or its negation -xi.
In this problem, the negation of a literal ;Xi is the negation of xi, denoted -;Xi, and
the negation of -'Xi is Xi. That is, when negating -'Xi, first form ---Xi, and then drop
the double negation sign.
Given a 2-CNF formula Oo, construct a digraph as follows: The vertices are all
literals X-i and -.ki where Xi is a propositional variable in the program. For each clause
Xi v•Xj, add directed edges from vertex -'Xi to vertex Xj and from vertex -Xj to )q.
(a) Draw the digraph constructed for the sample formulas 0 and X given previously.
(b) Show that for literals XI and k 2 , if there is a directed trail from vertex X- 1 to vertex
X 2 , then 0 • k I --- k 2.
(c) Call a strongly connected component of the graph self-contradictory if it includes
both Xi and -Xi, for some literal Xi. Show that if the graph has a self-contradictory,
strongly connected component, then tk is unsatisfiable.
(d) Use part c to show that formula 0o is unsatisfiable.
(e) For a directed graph G, define a binary relation -< on the strongly connected com-
ponents of the graph as follows: C1 i C 2 if there are vertices al E C, and a2 E C 2
where there is a directed trail in G from al to a2. Show that if C 1 -< C 2 , then for
every vertex al E C 1 and every vertex a2 E C 2 , there is a directed trail in G from
a to a2. (Remember that there is always a directed trail, of length zero, from any
vertex to itself.)
(f) Continue part e: Show that -< is a partial ordering of the strongly connected com-
ponents of G.
(g) Return to the graph defined from the 2-CNF formula x. Since the formula has only
finitely many proposition letters, it has only finitely many literals, and the graph
has only finitely many strongly connected components. For the partial ordering -<
defined in part e, pick a strongly connected component Co that is minimal in the
ordering.
Assume that Co is not self-contradictory. Start constructing a truth assignment
for 0 by setting each literal in Co to FALSE-that is, if xi E Co, set xo to FALSE,
and if --xi e Co, set xi to TRUE. Show that if c is any clause of (P, either this
assignment sets one of the literals in c to TRUE or this assignment does not assign
truth values to any literal in the clause. (Such a partial truth assignment is called
an autark assignment.)
(h) Challenge: Prove the converse of part c. (Hint: Use induction.)
(i) Challenge: Earlier, we presented an algorithm to check whether a 2-CNF for-
mula is unsatisfiable: Form the graph, find the strongly connected components,
and check whether any strongly connected component is self-contradictory. Ana-
lyze the complexity of this algorithm.