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}\]

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.




Related posts