22
$\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$
1
  • 8
    $\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$ Jul 8, 2011 at 19:20

5 Answers 5

34
$\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$
5
  • 6
    $\begingroup$ Careful. Who says the input to SAT has to have "clauses"? $\endgroup$
    – Jeffε
    Jul 3, 2011 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$ Jul 3, 2011 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, 2011 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, 2011 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, 2019 at 18:23
29
$\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$
21
$\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$
16
$\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$
2
  • 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, 2014 at 4:25
  • $\begingroup$ @crockeea If I had to guess, some algorithms are easier to implement if you assume 3-SAT clauses contain 3 unique variables per clause $\endgroup$ Jun 12, 2020 at 14:12
2
$\begingroup$

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

$\endgroup$
1
  • $\begingroup$ To generalize, if we assume all logical operators are binary or unary, then we substitute out binary operators with a single variable (similar to this answer) until we have 3-SAT. For example, if your formula contains (!y => !z) you may define x <=> (!y => !z) $\endgroup$ Jun 12, 2020 at 14:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.