Direct SAT to 3-SAT reduction

Question

Here the goal is to reduce an arbitrary SAT problem to 3-SAT in polynomial time using the fewest number of clauses and variables. My question is motivated by curiosity. Less formally, I would like to know: "What is the 'most natural' reduction from SAT to 3-SAT?"

Now the reduction that I've always seen in text books goes something like this:

1. First take your instance of SAT and apply the Cook-Levin theorem to reduce it to circuit SAT.

2. Then you finish the job by the standard reduction of circuit SAT to 3-SAT by replacing gates with clauses.

While this works, the resulting 3-SAT clauses end up looking almost nothing like the SAT clauses you started with, due to the initial application of the Cook-Levin theorem.

Can anyone see how to do the reduction more directly, skipping the intermediate circuit step and going directly to 3-SAT? I would even be happy with a direct reduction in the special case of n-SAT.

(I would guess that there are some trade-offs between computation time and the size of the output. Clearly a degenerate -- though fortunately inadmissible unless P=NP -- solution would be to just solve the SAT problem, then emit a trivial 3-SAT instance...)

EDIT: Based on ratchet's answer it is clear now that the reduction to n-SAT is somewhat trivial (and that I really should have thought that one through a bit more carefully before posting). I'm leaving this question open for a bit in case someone knows the answer to the more general situation, otherwise I will simply accept ratchet's answer.

Answer 1

Each SAT clause has 1, 2, 3 or more variables. The 3 variable clause can be copied with no issue

The 1 and 2 variable clauses {a1} and {a1,a2} can be expanded to {a1,a1,a1} and {a1,a2,a1} respectively.

The clause with more than 3 variables {a1,a2,a3,a4,a5} can be expanded to {a1,a2,s1}{!s1,a3,s2}{!s2,a4,a5} with s1 and s2 new variables whose value will depend on which variable in the original clause is true

Answer 2

This is probably beyond the scope of the question, but I wanted to post it anyway. Using techniques from parameterized complexity it has been proven that, assuming the polynomial hierarchy doesn't collapse to its third level, there is no polynomial-time algorithm which takes an instance of CNF-SAT on n variables with unbounded clause length, and outputs an instance of k-CNF-SAT (no clauses of length more than k) on n' variables where $n'$ is polynomial in $n$. This follows from work of Fortnow and Santhanam, see also follow-up work by Dell and van Melkebeek. So roughly speaking, the number of variables in the k-CNF-SAT instance will always depend on the number of clauses in your CNF-SAT formula.

Answer 3

If you need a reduction from k-SAT to 3-SAT, then ratchet's answer works fine.

If you want a direct reduction from generic propositional formula to CNF (and to 3-SAT) then - at least from the "SAT solvers perspective" - I think that the answer to your question What is the 'most natural' reduction ...?, is: There is no 'natural' reduction!.

From the conclusions of Chapter 2 - "CNF Encodings" of the (very good) book: Handbook of Satisfiability:

...
There are usually many ways to model a given problem in CNF, and few guidelines are known for choosing among them. There is often a choice of problem features to model as variables, and some might take considerable thought to discover. Tseitin encodings are compact and mechanisable but in practice do not always lead to the best model, and some subformulae might be better expanded. Some clauses may be omitted by polarity considerations, and implied, symmetry breaking or blocked clauses may be added. Different encodings may have different advantages and disadvantages such as size or solution density, and what is an advantage for one SAT solver might be a disadvantage for another. In short, CNF modelling is an art and we must often proceed by intuition and experimentation.
...

The most known algorithm is the Tseitin algorithm (G. Tseitin. On the complexity of derivation in propositional calculus. Automation of Reasoning: Classical Papers in Computational Logic, 2:466–483, 1983. Springer-Verlag.)

For a good introduction to CNF encodings read the suggested book Handbook o Satisfiability. You can also read some recent works and look at the references; for example:

• P. Jackson and D. Sheridan. Clause form conversions for Boolean circuits. In H. H. Hoos and D. G. Mitchell, editors, Theory and Applications of Satisfiability Testing, 7th International Conference, SAT 2004, volume 3542 of LNCS, pages 183–198. Springer, 2004. (which aims to reduce the number of clauses)
• P. Manolios, D. Vroon, Efficient Circuit to CNF Conversion. In Theory and Applications of Satisfiability Testing – SAT 2007 (2007), pp. 4-9

Answer 4

Let me please post another solution similar to Ratchel's but somewhat different. This is directly taken from chapter 9 of the 2nd Edition of "The Algorithm Design Manual" by Steven Skiena

• If the clause has only one literal C={z1}, then create two new variables v1 and v2 and four new 3-literal clauses: {v1, v2, z1}, {!v1, v2, z1}, {v1, !v2, z1} and {!v1, !v2, z1}. Note that the only way that all four of these clauses can be simultaneously satisfied is if z1=T, which also means the original C will be satisfied
• If the clause has two literals, C={z1, z2}, then create one new variable v1 and two new clauses: {v1, z1, z2} and {!v1, z1, z2}. Again, the only way to satisfy both of these clauses is to have at least one of z1 and z2 be true, thus satisfying C
• If the clause has three literals, C={z1, z2, z3}, just copy C into the 3-SAT instance unchanged
• If the clause has more than 3 literals C={z1, z2, ..., zn}, then create n-3 new variables and n-2 new clauses in a chain, where for 2<= j <= n-2, Cij={v1,j-1, zj+1,!vi,j}, Ci1={z1, z2, !vi,1} and Ci,n-2={vi,n-3, zn-1, zn}

Answer 5

Given a SAT clause of literals x1 or x2 or ... or xn, we can replace out 2 literals a, b as follows.

Introduce a new variable, c.

Let:

c <=> (a or b)

Replace a or b in the clause with c. The resulting clause has one less literal.

We need to convert that into CNF. First break that up into these two clauses:

c => (a or b)
(a or b) => c

Now we need to get rid of the =>.

(c => (a or b))
<=> (!c or a or b)
<=> (a or b or !c)

That one is done.

((a or b) => c)
<=> (!(a or b) or c)
<=> ((!a and !b) or c)
<=> (a or !b or c) and (!a or b or c) and (!a or !b or c)

You can check that derivation with a truth table.

Therefore, by adding 4 clauses (a or b or !c) and (a or !b or c) and (!a or b or c) and (!a or !b or c) we can substitute out two variables with one.

We can iteratively apply this process on each clause until it's of size at most 3.

To get clauses at least size 3, see this answer. This assumes duplicate literals are okay.

To get clauses at least size 3 without duplicate literals see this answer