9

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

Community
  • 1
Xavier Labouze
  • 1,117
  • 1
  • 9
  • 27
  • By equivalent you mean equi-satisfiable, I assume? – Jan Johannsen Nov 15 '13 at 09:10
  • 1
    Rather, "with the same set of models". – Xavier Labouze Nov 15 '13 at 09: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. – Marzio De Biasi 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...) – Xavier Labouze Nov 15 '13 at 23:58
  • @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 Nov 16 '13 at 00:00
  • looks fairly similar to finding the shortest equivalent CNF formula – vzn Nov 16 '13 at 00:05
  • @vzn- Not quite, here the clauses are limited in size (Tks for the link). – Xavier Labouze Nov 16 '13 at 00:17

1 Answers1

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.

Marzio De Biasi
  • 22,915
  • 2
  • 58
  • 127
  • 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 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? – Marzio De Biasi 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)$. – Xavier Labouze 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? – Ilya Gazman Dec 24 '13 at 08:27
  • 1
    $\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 Dec 24 '13 at 15:10