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.

  • $\begingroup$ This is essentially the NP-hardness proof of 3SAT. See for example this answer on Mathematics. $\endgroup$ Mar 23, 2022 at 13:34
  • $\begingroup$ Yes, I understand how to transform 1-SAT and 2-SAT to 3-SAT but I don't understand how to do it with k>3. I read the answer on mathematics but I don't understand sorry. I need an example. $\endgroup$ Mar 23, 2022 at 16:11
  • $\begingroup$ Gadi A.’s answer explains precisely how to do it. $\endgroup$ Mar 23, 2022 at 18:48
  • $\begingroup$ Thank you for your post. I edited my post. Do you have a reference which explained the method (why it works for k>3?). (a|b|c|...|y|z)=(a|b|A)∧( A|c|B)∧( B|d|C)∧...∧( V|x|W)∧( W|y|z) $\endgroup$ Mar 25, 2022 at 7:31
  • $\begingroup$ The method, as you describe it, doesn’t work. The new variables should appear once positively, once negatively. It is then an exercise to figure out why it works. $\endgroup$ Mar 25, 2022 at 8:21

1 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.

  • $\begingroup$ Thank you. I can't vote because I don't have the reputation but when I'll go it, I will vote. $\endgroup$ Mar 26, 2022 at 9:06
  • $\begingroup$ Another way I think is useful to look at this is through resolution. Resolution on the first two clauses eliminates y_2 and gives (x_1 ∨ x_2 ∨ x_3 ∨ y_3). Continue this process and the original clause is recovered, and therefore logically implied. $\endgroup$
    – GManNickG
    Mar 27, 2022 at 1:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.