# What are known 3SAT to 2SAT reductions?

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)

• 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). – D.W. Jul 6 '18 at 18:33
• 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. – D.W. Jul 6 '18 at 18:34

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.