10
$\begingroup$

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

Improve this question
$\endgroup$
8
  • $\begingroup$ By equivalent you mean equi-satisfiable, I assume? $\endgroup$
    – Jan Johannsen
    Commented Nov 15, 2013 at 9:10
  • 1
    $\begingroup$ Rather, "with the same set of models". $\endgroup$
    – Xavier Labouze
    Commented Nov 15, 2013 at 9:13
  • $\begingroup$ 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. $\endgroup$
    – vzn
    Commented Nov 15, 2013 at 16:18
  • $\begingroup$ 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. $\endgroup$
    – Marzio De Biasi
    Commented Nov 15, 2013 at 20:10
  • $\begingroup$ @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...) $\endgroup$
    – Xavier Labouze
    Commented Nov 15, 2013 at 23:58

1 Answer 1

Reset to default
7
$\begingroup$

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

Improve this answer
$\endgroup$
5
  • $\begingroup$ 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)$... $\endgroup$
    – Xavier Labouze
    Commented Nov 16, 2013 at 11:19
  • $\begingroup$ @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? $\endgroup$
    – Marzio De Biasi
    Commented Nov 16, 2013 at 13:49
  • $\begingroup$ 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)$. $\endgroup$
    – Xavier Labouze
    Commented Nov 16, 2013 at 15:40
  • $\begingroup$ 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? $\endgroup$
    – Ilya Gazman
    Commented Dec 24, 2013 at 8:27
  • 1
    $\begingroup$ $\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. $\endgroup$
    – Marzio De Biasi
    Commented Dec 24, 2013 at 15:10

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.