# Transform a CNF into an equivalent 3-CNF defined on the same variables

(I posted this question on CS ten days ago, with no answer since then - so I post it here.)

Any CNF formula can be transform in polynomial time into a 3-CNF formula by using new variables. It is not always possible if new variables are not allowed (take for instance the single clause formula : $(x_1 \lor x_2 \lor x_3 \lor x_4)$).

Let define the (SAT to 3-SAT) problem : Given $F$, a CNF formula. Is it possible to transform $F$ into an equivalent 3-CNF defined on the same variables as $F$ ? - where "equivalent" means with the same set of models.

What is the complexity of this problem ?

• By equivalent you mean equi-satisfiable, I assume? Nov 15 '13 at 9:10
• Rather, "with the same set of models". Nov 15 '13 at 9:13
• fyi tseitin transform is the name for the transform from $n$-SAT to 3-SAT using extra vars. it seems your question is something like asking about the existence of a compression algorithm for SAT. it sounds something like you want the same solutions by shortening the clauses to 3 or fewer variables. from EE, this is related to enumerating all the minterms and finding minimal covers and asking if any exists that fits the criteria (in this case all clauses 3 or fewer vars). it seems to have potentially high complexity.
– vzn
Nov 15 '13 at 16:18
• Perhaps it is co-NP-complete: pick a 3CNF formula $\varphi = C_1 \land ... \land C_n$, build a new formula $\varphi' = (y_1 \lor y_2 \lor y_3 \lor y_4) \land C_1 \land ... \land C_n$ with 4 new variables $y_1,...,y_4$. $\varphi'$ has a 3CNF equivalent formula on the same variables if and only if $\varphi$ is not satisfiable. Nov 15 '13 at 20:10
• @MarzioDeBiasi. Nice ! Yet, I am not sure it is sufficient to prove the co-NP completness (somehow, I expect a higher compexity but it is just an intuition...) Nov 15 '13 at 23:58

(From the comment above) The problem seems coNP-hard; the simple reduction is from 3CNF-UNSAT (which is coNP-complete): given a 3CNF formula $\varphi = C_1 \land ... \land C_m$, extend it adding a new clause with 4 new variables:

$$\varphi' = (y_1 \lor y_2 \lor y_3 \lor y_4) \land C_1 \land ... \land C_m$$

$\varphi'$ has an equivalent 3CNF formula defined on the same variables if and only if the original formula $\varphi$ is unsatisfiable.

($\Leftarrow$) the 3CNF formula $(y_1 \lor y_2 \lor y_3) \land (y_1 \lor y_2 \lor y_4) \land C_1 \land ... \land C_m$ is equivalent to $\varphi'$

($\Rightarrow$) suppose that $\varphi'$ has an equivalent 3CNF formula $\varphi''$ and that $\varphi$ is satisfiable. Pick a satisfying assignment $X = \langle \dot{x}_1,...,\dot{x}_n \rangle$ of $\varphi$, and simplify both $\varphi'$ and $\varphi''$ replacing the variables $x_i$ with the corresponding truth values $\dot{x}_i$. We get $\varphi'_X$ which is satisfiable if and only if $\varphi''_X$ is satisfiable (both contain only variables $y_i$). Clearly $\varphi'_X = (y_1 \lor y_2 \lor y_3 \lor y_4)$. Every clause of $\varphi''_X$ contains at most three variables, so we can pick one of them, e.g. $(y_1 \lor \lnot y_2 \lor y_3)$, and use it to build a satisfying assignment for $\varphi'$: $\langle y_1=false, y_2=true, y_3=false,y_4=true,\dot{x}_1,...,\dot{x}_n \rangle$ which is not a satisfying assignment for $\varphi''$, leading to a contradiction.

• Tks for the answer. I don't get the $(\Leftarrow)$ : I would have said that if $\varphi$ is unsastisfiable so is $\varphi'$, which then is equivalent to the empty clause (size 0). For the $(\Rightarrow$), just thinking if $\varphi = (x \lor \lnot x)$, then $(y_1 \lor y_2 \lor y_3 \lor y_4) \land (x \lor \lnot x)$ is equivalent to $(y_1 \lor y_2 \lor x)\land (y_3 \lor y_4 \lor \lnot x)$... Nov 16 '13 at 11:19
• @XavierLabouze: yes your $(\Leftarrow)$ seems better. In ($\Rightarrow)$ I assume that there is an equivalent 3CNF $\varphi'$, and then derive a contradiction from assuming that the original $\varphi$ is satisfiable. Do you think it's wrong? Nov 16 '13 at 13:49
• You are right - I was wrong in stating $(y_1 \lor y_2 \lor y_3 \lor y_4) \land (x \lor \lnot x)$ has the same set of models as $(y_1 \lor y_2 \lor x)\land (y_3 \lor y_4 \lor \lnot x)$. Nov 16 '13 at 15:40
• Did you notice that $(y_1 \lor y_2 \lor y_3) \land (y_1 \lor y_2 \lor y_4)$ is equal to $(y_1 \lor y_2) \land (y_3 \lor y_4)$? Can you explain this: "We get $\varphi'_X$ which is satisfiable if and only if $\varphi''_X$ is satisfiable", than you are adding "(both contain only variables $y_i$)", how can you be sure that they will only contain $y_i$? Also I don't understand the conclusion, did you proved that adding 4 variables clause to 3-cnf from the same variables is coNP-Complete? Dec 24 '13 at 8:27
• $\varphi_1 = (y_1 \lor y_2 \lor y_3) \land (y_1 \lor y_2 \lor y_4)$ and $\varphi_2 = (y_1 \lor y_2) \land (y_3 \lor y_4)$ are equisatisfiable but they are not equivalent (same set of models): y1=F,y2=F,y3=T,y4=T is a valid model for $\varphi_1$ but not for $\varphi_2$. In the question we are talking about equivalent formulas. The proof relies on the fact that $(y_1 \lor y_2 \lor y_3 \lor y_4)$ cannot have the same set of models of any 3CNF formulas. Dec 24 '13 at 15:10