NP-Completeness

Transformations and Satisfiability

11.1. Give the 3-SAT formula that results from applying the reduction of SAT to 3-SAT for the formula:

(x\lor y\lor {\overline {z}}\lor w\lor u\lor {\overline {v}})\land ({\overline {x}}\lor {\overline {y}}\lor z\lor {\overline {w}}\lor u\lor v)\land (x\lor {\overline {y}}\lor {\overline {z}}\lor w\lor u\lor {\overline {v}})\land (x\lor {\overline {y}})

Solution

11.2. Draw the graph that results from the reduction of 3-SAT to vertex cover for the expression

(x\lor {\overline {y}}\lor z)\land ({\overline {x}}\lor y\lor {\overline {z}})\land ({\overline {x}}\lor y\lor z)\land (x\lor {\overline {y}}\lor {\overline {x}})

11.3. Prove that 4-SAT is NP-hard.

Solution

11.4. Stingy SAT is the following problem: given a set of clauses (each a disjunction of literals) and an integer

k

, find a satisfying assignment in which at most

k

variables are true, if such an assignment exists. Prove that stingy SAT is NP-hard.

11.5. The Double SAT problem asks whether a given satisfiability problem has at least two different satisfying assignments. For example, the problem

{{v1,v2},{v_{1},v_{2}},{v_{1},v_{2}}}

is satisfiable, but has only one solution

(v_{1}=F,v_{2}=T)

. In contrast,

{{v_{1},v_{2}},{v_{1},v_{2}}}

has exactly two solutions. Show that Double-SAT is NP-hard.

Solution

11.6. Suppose we are given a subroutine that can solve the traveling salesman decision problem on page 357 in (say) linear time. Give an efficient algorithm to find the actual TSP tour by making a polynomial number of calls to this subroutine.

11.7. Implement a SAT to 3-SAT reduction that translates satisfiability instances into equivalent 3-SAT instances.

Solution

11.8. Design and implement a backtracking algorithm to test whether a set of clause sets is satisfiable. What criteria can you use to prune this search?

11.9. Implement the vertex cover to satisfiability reduction, and run the resulting clauses through a satisfiability solver code. Does this seem like a practical way to compute things?

Solution