<p>(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:</p>

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

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

<p>($\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'$</p>

<p>($\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.</p>

CC BY-SA 3.0
2013-11-16T11:19:42.000Z
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)$...
Xavier Labouze
CC BY-SA 3.0
2013-11-16T13:49:07.850Z
@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?
Marzio De Biasi
CC BY-SA 3.0
2013-11-16T15:40:34.120Z
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)$.
Xavier Labouze
CC BY-SA 3.0
2013-12-24T08:27:35.363Z
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?
Ilya Gazman
CC BY-SA 3.0
2013-12-24T15:10:40.427Z
$\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.
Marzio De Biasi
CC BY-SA 3.0
2013-11-16T07:50:24.360Z
2013-11-16T08:01:23.377Z
2013-11-16T08:01:23.377Z
Marzio De Biasi
<p>(I posted this question on <a href="https://cs.stackexchange.com/questions/16741/complexity-of-sat-to-3-sat-problem">CS</a> ten days ago, with no answer since then - so I post it here.)</p>

<p>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)$). </p>

<p>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 <em>on the same variables</em> as $F$ ? - where "equivalent" means with the same set of models.</p>

<p>What is the complexity of this problem ?</p>

CC BY-SA 3.0
2013-11-15T09:10:32.827Z
By equivalent you mean equi-satisfiable, I assume?
Jan Johannsen
CC BY-SA 3.0
2013-11-15T09:13:27.583Z
Rather, "with the same set of models".
Xavier Labouze
CC BY-SA 3.0
2013-11-15T16:18:07.113Z
fyi [tseitin transform](http://en.wikipedia.org/wiki/Tseitin-Transformation) 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
CC BY-SA 3.0
2013-11-15T20:10:11.843Z
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.
Marzio De Biasi
CC BY-SA 3.0
2013-11-15T23:58:01.757Z
@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...)
Xavier Labouze
CC BY-SA 3.0
2013-11-16T00:00:52.083Z
@vzn, yes the problem have probably high complexity (I would say co-NP complete at least), I haven't succeeded yet in finding it.
Xavier Labouze
CC BY-SA 3.0
2013-11-16T00:05:55.143Z
looks fairly similar to [finding the shortest equivalent CNF formula](http://cstheory.stackexchange.com/questions/9839/shortest-equivalent-cnf-formula)
vzn
CC BY-SA 3.0
2013-11-16T00:17:23.807Z
@vzn- Not quite, here the clauses are limited in size (Tks for the link).
Xavier Labouze
<cc.complexity-theory><complexity-classes><sat>
Transform a CNF into an equivalent 3-CNF defined on the same variables
Xavier Labouze
# Transform a CNF into an equivalent 3-CNF defined on the same variables

(Asked by: username_0 on 2013-11-15)

(I posted this question on [CS](https://cs.stackexchange.com/questions/16741/complexity-of-sat-to-3-sat-problem) 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 ?

**Tags:** cc.complexity-theory, complexity-classes, sat

> **Comments:**
> **username_1**: By equivalent you mean equi-satisfiable, I assume?  
> **username_0**: Rather, "with the same set of models".  
> **username_2**: fyi [tseitin transform](http://en.wikipedia.org/wiki/Tseitin-Transformation) 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.  
> **username_3**: 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.  
> **username_0**: @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...)  
> **username_0**: @username_2, yes the problem have probably high complexity (I would say co-NP complete at least), I haven't succeeded yet in finding it.  
> **username_2**: looks fairly similar to [finding the shortest equivalent CNF formula](http://cstheory.stackexchange.com/questions/9839/shortest-equivalent-cnf-formula)  
> **username_0**: @username_2- Not quite, here the clauses are limited in size (Tks for the link).  

---

## 1 answers

### Answer by username_3 on 2013-11-16. Score: 7

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

> **Comments:**
> **username_0**: 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)$...  
> **username_3**: @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?  
> **username_0**: 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)$.  
> **username_4**: 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?  
> **username_3**: $\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.  

---

