1
$\begingroup$

Is there a way to convert a 3SAT formula into a equisatisfiable 2SAT formula? Each method is of interest, even those that grow exponentially. (So if, for example, my 3SAT formula has 16 variables and 32 clauses, a transformed 2SAT formula would have 2ˆ16 variables and / or 2ˆ32 clauses)

An example of a 3SAT formula I would like to convert is:

A xor B xor C

Or the same in CNF:

(A or B or C) and (A or !B or !C) and (!A or !B or C) and (!A or B or !C)

$\endgroup$
  • $\begingroup$ Please edit your question to define what you mean. "any" is confusing. Here is a 3SAT formula: $(x_1 \lor x_2)$. That is trivially convertible to 2SAT. Here is another 3SAT formula: $(x_1 \lor x_2 \lor x_2)$. Also trivially convertible. Here is another: $(x_1) \land (\neg x_1)$. Also convertible to 2SAT. Ultimately any 3SAT formula is either satisfiable (hence can be converted to the 2SAT formula True) or not satisfiable (hence convertible to False). $\endgroup$ – D.W. Jul 6 '18 at 18:33
  • $\begingroup$ So please edit the question to define what you mean by "convertible", and clarify what you mean by "any" (are you asking if such a formula exists, or if there is a conversion procedure that works for all formula?). Also, do you have any other requirements on the conversion procedure? Is it legal for it to take exponential time? It would also help to tell us your thoughts, and what you have tried so far. As it stands the question looks straightforward, so it's hard to know what is preventing you from being able to answer it on your own. $\endgroup$ – D.W. Jul 6 '18 at 18:34
2
$\begingroup$

You seem to be asking about logically equivalent 2CNF functions rather than equisatisfiable ones. Not all Boolean formulae can be expressed as 2CNF formulae. Your example $(a \oplus b \oplus c)$ is one example of such a formula. $(a \lor b \lor c)$ is another. These formulae are simply not expressible equivalently in 2CNF, even with an exponential increase in formula size.

$\endgroup$
3
$\begingroup$

Yes, there is. Test whether the 3SAT formula is satisfiable or not. If it is, convert it to the formula True. If it is not, convert it to the formula False. This can be done in exponential time, e.g., by trying all possible assignments, or by your favorite method for testing satisfiability of a 3SAT formula.

Under the strong exponential-time hypothesis, this is optimal: there is nothing faster.

In particular, any procedure for converting into an equisatisfiable 2SAT formula can be used to test satisfiability of 3SAT: first convert into an equisatisfiable 2SAT formula, then test the satisfiability of the corresponding 2SAT formula (can be done in linear time. This gives a method for testing the satisfiability of a 3SAT formula, whose running time is essentially the same as the running time of the conversion procedure. Now the strong exponential-time hypothesis says that any method for testing satisfiability of 3SAT formulas requires exponential time. It follows that any method for conversion also requires exponential time.

$\endgroup$
  • $\begingroup$ Actually, I have read this article: cs.stackexchange.com/questions/18643/3-sat-to-2-sat-reduction/… And vzn said that you can reduce any 3SAT formula to a 2SAT formula with additional clauses and variables. Now I was wondering what such an encoding looks like. $\endgroup$ – Gregor K Jul 6 '18 at 19:55
  • $\begingroup$ @GregorK, as you can see in the comments there from David Richerby (and as my answer hopefully makes clear), you don't need additional clauses and variables. I can't tell what vzn had in mind, and vzn's answer did not elaborate, but there's no reason to add extra clauses if you don't need to; it seems rather pointless to me. (Also, as an aside, cstheory.stackexchange.com/a/27624/5038 seems to shed some doubt in my mind about whether there is any simple, useful, and natural encoding of that sort -- but I don't really want to get into that, given how pointless it is anyway.) $\endgroup$ – D.W. Jul 6 '18 at 20:54
  • $\begingroup$ So similarly, if we assume only P != NP, we still won't have a conversion algorithm in polynomial time... $\endgroup$ – xuq01 Jul 8 '18 at 12:32
  • $\begingroup$ @xuq01, correct. $\endgroup$ – D.W. Jul 9 '18 at 3:10

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.