Java Reference
In-Depth Information
strategy is to replace any clause C
i
that does not have exactly three literals
with a set of clauses each having exactly three literals. (Recall that
a
literal
can be a variable such as x, or the negation of a variable such as x.) Let
C
i
= x
1
+ x
2
+ ::: + x
j
where x
1
;:::;x
j
are literals.
1. j = 1, so C
i
= x
1
. Replace C
i
with C
0
i
:
(x
1
+ y + z) (x
1
+ y + z) (x
1
+ y + z) (x
1
+ y + z)
where y and z are variables not appearing in E. Clearly, C
0
i
is satisfi-
able if and only if (x
1
) is satisfiable, meaning that x
1
is
true
.
2. J = 2, so C
i
= (x
1
+ x
2
). Replace C
i
with
(x
1
+ x
2
+ z) (x
1
+ x
2
+ z)
where z is a new variable not appearing in E. This new pair of clauses
is satisfiable if and only if (x
1
+ x
2
) is satisfiable, that is, either x
1
or
x
2
must be true.
3. j > 3. Replace C
i
= (x
1
+ x
2
+ + x
j
) with
(x
1
+ x
2
+ z
1
) (x
3
+ z
1
+ z
2
) (x
4
+ z
2
+ z
3
) :::
(x
j2
+ z
j4
+ z
j3
) (x
j1
+ x
j
+ z
j3
)
where z
1
;:::;z
j3
are new variables.
After appropriate replacements have been made for each C
i
, a Boolean
expression results that is an instance of 3 SAT. Each replacement is satisfi-
able if and only if the original clause is satisfiable. The reduction is clearly
polynomial time.
For the first two cases it is fairly easy to see that the original clause
is satisfiable if and only if the resulting clauses are satisfiable. For the
case were we replaced a clause with more than three literals, consider the
following.
1. If E is satisfiable, then E
0
is satisfiable: Assume x
m
is assigned
true
. Then assign z
t
;t m 2 as
true
and z
k
;t m 1 as
false
. Then all clauses in Case (3) are satisfied.
2. If x
1
;x
2
;:::;x
j
are all
fal
se
, then z
1
;z
2
;:::;z
j3
are all
true
. But
then (x
j1
+ x
j2
+ z
j3
) is
false
.
2
Next we define the problem VERTEX COVER for use in further examples.
VERTEX COVER:
Input: A graph G and an integer k.
Output: YES if there is a subset S of the vertices in G of size k or less such
that every edge of G has at least one of its endpoints in S, and NO otherwise.
