It is well known that any CNF formula can be transform in polynomial time into a 3-CNF formula by using new variables (see here). If using new variables is not allowed, it is not always possible (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 ?

Edit : It has been shown on cstheory that the problem is co-NP hard.

  • 5
    $\begingroup$ It is not always possible to transform $F$, a general CNF formula defined on $n$ variables, into a 3-CNF formula defined on the same $n$ variables as $F$. $\endgroup$ – Xavier Labouze Nov 5 '13 at 16:07
  • 4
    $\begingroup$ Just pick a single clause formula $F = x_1 \lor x_2 \lor x_3 \lor x_4$ $\endgroup$ – Vor Nov 5 '13 at 16:32
  • $\begingroup$ It is possible after solving the sat. Then you can construct any k-sat without adding new variables. So the complexity of this problem is the complexity of solving sat. $\endgroup$ – Ilya Gazman Dec 22 '13 at 10:27
  • $\begingroup$ @Babibu - Can you elaborate ? (I have just edited the question to link it with the answer on cstheory which shows that the problem is co-np hard and to precise that "equivalent" means with the same set of models). $\endgroup$ – Xavier Labouze Dec 23 '13 at 22:56
  • $\begingroup$ What do you mean by transform ? I think there is a PSPACE upper bound if the problem is to check the existence of a 3CNF formula equivalent (with the same set of models) to a given formula in CNF $\endgroup$ – Pablo Munoz Dec 24 '13 at 17:11

This has been answered on the CS Theory StackExchange site: https://cstheory.stackexchange.com/a/19833/5038

(I'm posting an answer here, so this question does not get treated as a question-without-an-answer and get periodically rotated back onto the front page by the Community user. Normally, questions without any upvoted or accepted answer are re-displayed on the front page every so often. Since this question now has been solved answered elsewhere, there doesn't seem any need for that. As long as someone upvotes or accepts this answer, that should prevent this question from being rotated back onto the front page. I'm ticking the community wiki box so I won't get any rep from this answer.)

  • $\begingroup$ Tks for your concern: +1 $\endgroup$ – Xavier Labouze Dec 27 '13 at 16:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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