I am wondering about expressing $3SAT$ clause (disjunction of 3 literals) as a $2SAT$ formula. If it would be possible then $P=NP$
Let's consider a clause of the form: $x_1 \vee x_2 \vee x_3$
The question is: is there a $2SAT-CNF$ encoding of the constraint that at least one of the $x1, x2, x3$ is $true$ ? (possibly such encoding can use a lot of additional variables and clauses…) I am curious if anybody has proven that such encoding simply does not exist.
More background: I recently went through following paper: SAT Encodings of the At-Most-k Constraint
Just wondering what can be encoded purely within $2SAT$
Best Answer
Suppose you have a representation of $x_1\lor x_2\lor x_3$ as 2CNF clauses, possibly involving with hidden variables. (This would "represent" the three-way disjunction in the sense that the 2CNF is satisfiable together with any consistent combination of $(\neg)x_i$ that contains at least one positive $x_i$, and is not satisfiable together with $\neg x_1 \land \neg x_2 \land \neg x_3$.
First any hidden variable $h$ can be eliminated by replacing all clauses involving $h$ or $\neg h$, by the result of applying resolution to every combination of such clauses that has $h$ in one and $\neg h$ in another. This does not change the satisfiability of the formula. (Here an important observation is that using resolution on two 2-clauses produces another 2-clause; the is not true for clauses of higher arity).
Thus, without loss of generality we can assume that there are no hidden variables -- and the question is then just whether any 2CNF in the variables $x_1, x_2, x_3$ is logically equivalent to $x_1\lor x_2\lor x_3$.
We can easily see that this is not the case. Any nontrivial 2-clause will be true for at most $6$ of the $8$ different truth valuations of $x_1, x_2, x_3$. Taking the conjunction of several such clauses cannot make more valuations come out true -- but $x_1\lor x_2\lor x_3$ is true in $7$ cases, so it is not equivalent to any 2CNF.