3SAT

Summary

We show that we can break up larger clauses into clauses of size 3 to reduce SAT problems to 3SAT problems. This lets us prove that 3SAT is at least as hard as SAT, which is known to be NP-Complete.

Contents

• 3SAT Problem Definition
• Proof Outline
• 3SAT in NP
• Reduce SAT to 3SAT
• Example
  • Proof
    • Forward claim
    • Reverse claim
    • Correctness

3SAT Problem Definition

Input: Boolean formula f in CNF with n variables and m clauses where each clause has at most 3 literals

Output: Satisyfing assignment if one exists, otherwise, NO

Proof Outline

Show that 3SAT is NP-Complete

Need to show:

• 3SAT $\in$ NP
• SAT $\rightarrow$ 3SAT
  • thus, $\forall p \in NP, p \rightarrow \text{3SAT}$

3SAT in NP

Given a 3SAT input f, and T/F assignment for $x_1, \ldots, x_n$, for each clause $c \in f$:

• in O(1) time check that at least one literal in c is satisfied

O(m) total time

Reduce SAT to 3SAT

Take input f for SAT, and transform it into f’ for 3SAT problem.

Take output o’ for 3SAT, and transform it into o for SAT problem.

Need o’ satisfies f’ $\iff$ o satisfies f

Example

$\begin{gathered} f = & \left( x_3 \right) \land & \left( \bar{x_2} \lor x_3 \lor \bar{x_1} \lor \bar{x_4} \right) \land & \left( x_2 \lor x_1 \right) \ & c_1 & c_2 & c_3 \end{gathered}$

Becomes

$\begin{gathered} f = & \left( x_3 \right) \land & \left\lbrace\left( \bar{x_2} \lor x_3 \lor y \right) \land \left(\bar{y} \lor \bar{x_1} \lor \bar{x_4} \right)\right\rbrace \land & \left( x_2 \lor x_1 \right) \ & c_1 & c_2 & c_3 \end{gathered}$

Proof

We need to prove that c is satisfiable if and only if c’ is satisfiable

Forward claim

Take a satisfying assignment for c

if $x_2 = F \text { or } x_3 = T$: then set $y = F$ to satisfy the second clause

if $x_1 = F \text { or } x_4 = F$: then set $y = F$ to satisfy the first clause

Reverse claim

Take satisfying assignment for c’

if $y = T$: then $x_1 = F \text{ or } x_4 = F$

if $y = F$: then $x_2 = F \text{ or } x_3 = T$

Correctness

Since we create a chain of introducing an auxilliary variable (y) at the tail of all but the last clause, and negate that variable in the head of the next clause, it’s impossible to create a satisfying assignment SOLELY on these new variables, since setting one to true will satisfy one clause and not the next. If we set them all to true, that will set the last clause to false, so we still need at least one of the original variables to be true in the last clause.