<p>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&#39;$ is polynomial in $n$. This follows from work of <a href="http://dx.doi.org/10.1016/j.jcss.2010.06.007">Fortnow and Santhanam</a>, see also follow-up work by <a href="http://www2.informatik.hu-berlin.de/~dell/papers/dvm10sparsification.pdf">Dell and van Melkebeek</a>. 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.</p>

CC BY-SA 3.0
2011-07-04T12:12:02.587Z
2011-07-04T12:12:02.587Z
Bart Jansen
<p>If you need a reduction from k-SAT to 3-SAT, then ratchet's answer works fine.</p>

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

<p>From the conclusions of <em>Chapter 2 - "CNF Encodings"</em> of the (very good) book: <a href="http://www.st.ewi.tudelft.nl/sat/handbook/">Handbook of Satisfiability</a>:</p>

<p>...<br>
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. <strong>In short, CNF modelling
is an art and we must often proceed by intuition and experimentation.</strong>
<br>...</p>

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

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

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

CC BY-SA 3.0
2011-07-03T18:27:23.207Z
2011-07-03T18:27:23.207Z
Marzio De Biasi
<p>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 <a href="http://www.algorist.com" rel="noreferrer">"The Algorithm Design Manual"</a> by Steven Skiena</p>

<ul>
<li>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</li>
<li>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</li>
<li>If the clause has three literals, C={z1, z2, z3}, just copy C into the 3-SAT instance unchanged</li>
<li>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&lt;= j &lt;= 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}</li>
</ul>

CC BY-SA 3.0
2014-12-01T04:25:16.417Z
@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?
crockeea
CC BY-SA 4.0
2020-06-12T14:12:24.730Z
@crockeea If I had to guess, some algorithms are easier to implement if you assume 3-SAT clauses contain 3 unique variables per clause
Jesus is Lord
CC BY-SA 3.0
2011-11-26T00:37:19.617Z
2017-07-07T18:14:05.220Z
2017-07-07T18:14:05.220Z
Carlos Linares López
<p>Given a SAT clause of literals <code>x1 or x2 or ... or xn</code>, we can replace out 2 literals <code>a</code>, <code>b</code> <strong>as follows.</strong></p>

<p>Introduce a new variable, <code>c</code>.</p>

<p>Let:</p>

<p><code>c &lt;=&gt; (a or b)</code></p>

<p>Replace <code>a or b</code> in the clause with <code>c</code>. The resulting clause has one less literal.</p>

<p>We need to convert that into CNF. First break that up into these two clauses:</p>

<pre><code>c =&gt; (a or b)
(a or b) =&gt; c
</code></pre>

<p>Now we need to get rid of the <code>=&gt;</code>.</p>

<pre><code>(c =&gt; (a or b))
&lt;=&gt; (!c or a or b)
&lt;=&gt; (a or b or !c)
</code></pre>

<p>That one is done.</p>

<pre><code>((a or b) =&gt; c)
&lt;=&gt; (!(a or b) or c)
&lt;=&gt; ((!a and !b) or c)
&lt;=&gt; (a or !b or c) and (!a or b or c) and (!a or !b or c)
</code></pre>

<p>You can check that derivation with a <a href="https://web.stanford.edu/class/cs103/tools/truth-table-tool/" rel="nofollow noreferrer">truth table</a>.</p>

<p><strong>Therefore, by adding 4 clauses <code>(a or b or !c) and (a or !b or c) and (!a or b or c) and (!a or !b or c)</code> we can substitute out two variables with one.</strong></p>

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

<p>To get clauses at least size 3, see <a href="https://cstheory.stackexchange.com/a/7215/58255">this answer</a>. This assumes duplicate literals are okay.</p>

<p>To get clauses at least size 3 without duplicate literals see <a href="https://cstheory.stackexchange.com/a/9135/58255">this answer</a></p>

CC BY-SA 4.0
2020-06-12T14:56:40.010Z
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)`
Jesus is Lord
CC BY-SA 4.0
2020-06-12T14:44:31.967Z
2020-06-12T15:03:42.203Z
2020-06-12T15:03:42.203Z
Jesus is Lord
<p>Each SAT clause has 1, 2, 3 or more variables. The 3 variable clause can be copied with no issue</p>

<p>The 1 and 2 variable clauses <code>{a1}</code> and <code>{a1,a2}</code> can be expanded to <code>{a1,a1,a1}</code> and <code>{a1,a2,a1}</code> respectively.</p>

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

CC BY-SA 3.0
2011-07-03T16:21:26.063Z
Careful.  Who says the input to SAT has to have "clauses"?
Jeffε
CC BY-SA 3.0
2011-07-03T17:50:52.833Z
The question said "I would even be happy with a direct reduction in the special case of n-SAT"
Ryan Williams
CC BY-SA 3.0
2011-07-03T22:21:53.957Z
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.
Mikola
CC BY-SA 3.0
2011-07-03T23:02:18.013Z
@Mikola Maybe the Tseitin or Plaisted-Greenbaum transformation give you 3CNF? (I'm not quite sure I understand the question fully  :) )
Mikolas
CC BY-SA 4.0
2019-09-06T18:23:36.920Z
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.
KGhatak
CC BY-SA 3.0
2011-07-03T13:24:04.527Z
2017-11-27T07:35:53.387Z
2017-11-27T07:35:53.387Z
ratchet freak
<p>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?"</p>

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

<ol>
<li><p>First take your instance of SAT and apply the Cook-Levin theorem to reduce it to circuit SAT.</p></li>
<li><p>Then you finish the job by the standard reduction of circuit SAT to 3-SAT by replacing gates with clauses.  </p></li>
</ol>

<p>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.</p>

<p>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.</p>

<p>(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...)</p>

<p>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.</p>

CC BY-SA 3.0
2011-07-08T19:20:14.017Z
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?
Luca Trevisan
<cc.complexity-theory><sat><reductions>
Direct SAT to 3-SAT reduction
Mikola
# Direct SAT to 3-SAT reduction

(Asked by: username_0 on 2011-07-03)

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.

**Tags:** cc.complexity-theory, sat, reductions

> **Comments:**
> **username_1**: 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?  

---

## 5 answers

### Answer by username_7 on 2011-07-03. Score: 34 | Accepted answer

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

> **Comments:**
> **username_8**: Careful.  Who says the input to SAT has to have "clauses"?  
> **username_9**: The question said "I would even be happy with a direct reduction in the special case of n-SAT"  
> **username_0**: 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.  
> **username_10**: @username_0 Maybe the Tseitin or Plaisted-Greenbaum transformation give you 3CNF? (I'm not quite sure I understand the question fully  :) )  
> **username_11**: 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 'username_4' in his/her post here.  

---

### Answer by username_2 on 2011-07-04. Score: 30

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](http://dx.doi.org/10.1016/j.jcss.2010.06.007), see also follow-up work by [Dell and van Melkebeek](http://www2.informatik.hu-berlin.de/~dell/papers/dvm10sparsification.pdf). 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 by username_3 on 2011-07-03. Score: 21

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](http://www.st.ewi.tudelft.nl/sat/handbook/):

...  
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 by username_4 on 2011-11-26. Score: 16

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"](http://www.algorist.com) 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}

> **Comments:**
> **username_5**: @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?  
> **username_6**: @username_5 If I had to guess, some algorithms are easier to implement if you assume 3-SAT clauses contain 3 unique variables per clause  

---

### Answer by username_6 on 2020-06-12. Score: 2

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

> **Comments:**
> **username_6**: 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)`  

---

