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.