# Why can't 3-SAT be solved efficiently if you convert all clauses (x ∨ y ∨ z) into (u ∨ z) by introducing a variable?

Let $$a_i$$, $$b_i$$, etc., be a literal, i.e., a variable or the negation of a variable.

3-SAT concerns formulas in CNF form: $$(a_1 \vee a_2 \vee a_3) \wedge \dots \wedge (b_1 \vee b_2 \vee b_3)$$ (3-CNF). The problem of whether or not such a formula has an assignment of its Boolean variables such that it evaluates to $$1$$ is NP-complete.

But if we can convert the 3-CNF formula into a 2-CNF efficiently, then using implication graphs, we know that 2-SAT is in the complexity class P, which would make 3-SAT lives there as well.

So I'm wondering what are the obstacles to doing this?

For example, why can't we do this to remedy it (working with a clause at a time):

$$F := (a \vee b \vee c) \\ u := (a \vee b) \\ \text{But, this assignment (equality) is true} \iff \\ G := (u \vee \bar{a}) \wedge (u \vee \bar{b}) \wedge (\bar{u} \vee a) \wedge (\bar{u} \vee b) =1. \\ \text{ So, } F = 1 \iff \exists u~(u\vee c) \wedge G = 1.$$

And all we've done is swapped out one 3-CNF clause in favor of 5 2-CNF clauses.

I'm not seeing why this wouldn't make 3-SAT polynomial time.

• While this approach does not work (as explained by John L) to reduce 3-SAT to 2-SAT, something very similar does indeed work to reduce even longer clauses longer down to 3-SAT. This means that 3-SAT is equivalent to general SAT, which allows any size of clause. Aug 17, 2022 at 9:20

$$u = (a \vee b) \iff (u \vee \bar{a}) \wedge (u \vee \bar{b}) \wedge (\bar{u} \vee a) \wedge (\bar{u} \vee b) =1$$

Unfortunately, the equivalence above does not hold.

Let $$a=\text{false}$$, $$b=\text{true}$$, $$u=\text{true}$$.

• the LHS is $$\text{true}$$.
• the RHS is $$\text{false}$$ since $$\bar u\lor a=\text{false}\lor\text{false}=\text{false}$$.

In fact, we can prove the following.
Claim: there is no 2-CNF formula $$\varphi(a,b,c,x_1,\cdots,x_m)$$ such that $$\forall a, b, c\in\{\text{false, true}\}$$, $$a\lor b\lor c \iff \exists x_1 \cdots \exists x_m ~\varphi(a,b,c,x_1,\ldots,x_m).$$

• For the proof of the claim, use the fact that majority on three inputs is a polymorphism of width-2 clauses but not of width-3 clauses. Aug 16, 2022 at 20:59