Complexity of (SAT to 3-SAT) Problem?

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.

• 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$. Nov 5 '13 at 16:07
• Just pick a single clause formula $F = x_1 \lor x_2 \lor x_3 \lor x_4$
– Vor
Nov 5 '13 at 16:32
• 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. Dec 22 '13 at 10:27
• @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). Dec 23 '13 at 22:56
• 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 Dec 24 '13 at 17:11