Notes - Logic and Proof MT24, 3-CNF formulas
Flashcards
The $\mathbf{3SAT}$ decision problem is:
- Input: 3CNF formula $\Phi$ (each clause has at most three literals)
- Output: Is $\Phi$ satisfiable?
The $\textbf{SAT}$ decision problem is:
- Input: CNF formula $\Phi$
- Output: Is $\Phi$ satisfiable?
@Prove that
\[\mathbf{SAT} \le \mathbf{3SAT}\]
- Input: 3CNF formula $\Phi$ (each clause has at most three literals)
- Output: Is $\Phi$ satisfiable?
- Input: CNF formula $\Phi$
- Output: Is $\Phi$ satisfiable?
Suppose we have a CNF formula $\Phi$. Then we can convert it into an equivalent 3CNF formula by adding appropriate extra variables, e.g.
\[(a \vee b \vee c \vee d \vee e) \mapsto (a \vee b \vee q_1) \wedge (\overline{q_1} \vee c \vee q_2) \wedge (\overline q_2 \vee d \vee e)\]Since this can be done in polynomial time, we are done.
In more detail, pick some clause $C$. If $C$ has one literal, say $\ell$. Let $q _ 1$ and $q _ 2$ be two new variables, then we can replace $C$ by
\[(\ell \vee q_1 \vee q_2) \wedge (\ell \vee q_1 \vee \overline{q_2} ) \wedge (\ell \vee \overline{q_1} \vee q_2 ) \wedge (\ell \vee \overline{q_1} \vee \overline{q_2} )\](Here $q _ 1$ and $q _ 2$ cycle through all possible truth assignments, so that we require $\ell$ to be satisfied).
If $C$ has two literals, replace $C$ by
\[(\ell \vee q_1) \wedge (\ell \vee \overline{q_1})\]If $C$ has three literals, we don’t need to do anything.
If $C$ has more than three literals, we have $C = \ell _ 1 \vee \ell _ 2 \vee \cdots \vee l _ k$ for $k > 3$. Let $q _ 1, \cdots, q _ {n-3}$ be $n-3$ new variables. Replace $C$ by
\[(\ell_1 \vee \ell_2 \vee q_1) \wedge (\ell_3 \vee \overline{q_1} \vee q_2) \wedge (\ell_4\vee \overline{q_2} \vee q_3) \wedge \cdots \wedge (\ell_{k-2} \vee \overline{q_{k-4} } \vee q_{k-3}) \vee (\ell_{k-1} \wedge \ell_k \wedge \overline {q_{k-3} })\]If there is a satisfying assignment of $C$, we can satisfy this clause by toggling $q$ appropriately, and if there is a satisfying assignment of the new clause, we can likewise find a satisfying assignment of the original.