CNF clause to 3-SAT

Question

How to transform a k-SAT CNF clause into a combination of 2-SAT and/or 3-SAT (1-SAT) clauses? $k>3$

Example 5-SAT: $$ Q = \neg A \lor B \lor C \lor D \lor E $$ $$ \; \; = (X0 \lor X2 \lor X3) \land (Y1 \lor Y2 \lor Y3) \land \; ... $$

Do I have to apply Tseytin transformation? How? Could you resolve my example, please?

---

EDIT From this answer. Thanks to Yuval Filmus

For simplicity: $\bar{x}$ is equivalent to $\neg x$ and $|$ is equivalent to $\lor$

1-SAT: Introduce 2 literals and cover the conjunction of all their combinations, to make sure at least one of these clauses is false if the original literal is. $$(A) = (A|m|n) \land (A|m|\bar{n}) \land (A|\bar{m}|n) \land (A|\bar{m}|\bar{n})$$ Idea: we add 2 variables m, n

2-SAT: Introduce 1 variable, and cover both its possible values. $$(A|B) = (A|B|m) \land (A|B|\bar{m})$$ Idea: we add 1 variable m

3-SAT: These are already in 3-SAT friendly form $$(A|B|C)$$

k-SAT (k<3): Split the literals into the first and the last pair, and work on all the single ones in between - as an example: $$(a|b|c|...|y|z) = (a|b|A) \land (\bar{A}|c|B) \land (\bar{B}|d|C) \land ...\land (~V|x|W) \land (~W|y|z)$$

Idea: we add k-3 variables. For 5-SAT, 2 new variables.

If I take my example, it gives: $$ Q = \bar{A} | B | C | D | E $$ $$ Q = (\bar{A} | B | ...) \land ... \land (...| D | E) $$ $$ = (\bar{A} | B | m) \land (\bar{m}| C | n) \land (\bar{n}| D | E) $$ with m and n, two new variables.

Could you give me more explanations about the k-SAT reduction. I don't really understand why it works.

Answer 1

We can express the clause $x_1 \lor x_2 \lor \cdots \lor x_n$ as the following conjunction of 3-clauses: $$ (x_1 \lor x_2 \lor y_2) \land (\lnot y_2 \lor x_3 \lor y_3) \land (\lnot y_3 \lor x_4 \lor y_4) \land \cdots \land (\lnot y_{n-2} \lor x_{n-1} \lor x_n), $$ where different $y$ variables are used for each clause.

To see that the two are equivalent (with respect to satisfiability), it suffices to check that $C_1 \lor C_2$ is equivalent to $(C_1 \land y) \lor (C_2 \land \lnot y)$. Suppose first that $C_1 \lor C_2$ is satisfied. If it is satisfied due to a literal in $C_1$, we can set $y$ to be false and satisfy $(C_1 \land y) \lor (C_2 \land \lnot y)$. Similarly, if $C_1 \lor C_2$ is satisfied due to a literal in $C_2$, we can set $y$ to true. For the other direction, suppose that $(C_1 \land y) \lor (C_2 \land \lnot y)$ is satisfied. If $y$ is false then $C_1$ must be satisfied, and if $y$ is true then $C_2$ must be satisfied. In both cases, $C_1 \lor C_2$ is satisfied.