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.