18
$\begingroup$

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.

$\endgroup$
  • 7
    $\begingroup$ I don't understand the use of Cook-Levin in (1). Isn't boolean-formula-SAT already a special case of circuit-SAT in which the graph structure of the circuit happens to be a tree? $\endgroup$ – Luca Trevisan Jul 8 '11 at 19:20
28
$\begingroup$

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

$\endgroup$
  • 6
    $\begingroup$ Careful. Who says the input to SAT has to have "clauses"? $\endgroup$ – Jeffε Jul 3 '11 at 16:21
  • 6
    $\begingroup$ The question said "I would even be happy with a direct reduction in the special case of n-SAT" $\endgroup$ – Ryan Williams Jul 3 '11 at 17:50
  • $\begingroup$ Yep, that works! I guess I should have thought a bit more carefully before adding that last line, but if I don't get an answer to the more general question I will accept this. $\endgroup$ – Mikola Jul 3 '11 at 22:21
  • 1
    $\begingroup$ @Mikola Maybe the Tseitin or Plaisted-Greenbaum transformation give you 3CNF? (I'm not quite sure I understand the question fully :) ) $\endgroup$ – Mikolas Jul 3 '11 at 23:02
  • $\begingroup$ I have been wondering why the extension specifically for k=1 mentioned by ratchet isn't appearing in any book (at least the ones I came across so far). My reasoning is that by definition a literal could be 'not a1' which cannot be extended like {a1, a1, a1}. On the other hand, you cannot do {'not a1', 'not a1', 'not a1]} as it needs another logic to identify if the original sat includes a negated literal or not. This is the reason (presumably) all authors including Michael R. Garey and David S. Johnson used a different extension presented by 'Carlos Linares López' in his/her post here. $\endgroup$ – KGhatak Sep 6 at 18:23
27
$\begingroup$

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.

$\endgroup$
19
$\begingroup$

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
$\endgroup$
15
$\begingroup$

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}
$\endgroup$
  • 1
    $\begingroup$ @TayfunPay Can you explain why you consider this solution to be more correct? Duplicating variables seems more natural to me, and doesn't violate any definition of 3SAT that I've seen. Is there some technicality that makes this solution better? $\endgroup$ – crockeea Dec 1 '14 at 4:25

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.