<p>The <a href="http://en.wikipedia.org/wiki/Circuit_minimization">circuit minization problem</a> is intractable (see the comments below). Also what I think you might be interested in is the technique some SAT solvers apply (at least to some degree) that is called SAT preprocessing. For example the well known MiniSAT solver uses a <a href="http://minisat.se/downloads/SatELite.pdf">CNF minimizer SatELite</a> to preprocess an instance. Google Scholar gives a lot of results for "sat preprocessing" as well.</p>

CC BY-SA 3.0
2012-01-22T21:56:53.330Z
I thought Buchfuhrer and Umans in 2008 settled the circuit minimization problem being $\Pi^p_2$-complete, under Turing reductions?
András Salamon
CC BY-SA 3.0
2012-01-23T10:10:24.503Z
Umans already showed in 1998 that finding a minimum equivalent CNF formula is $\Sigma^P_2$-hard (http://dx.doi.org/10.1006/jcss.2001.1775 ). The paper András mentions generalizes this to larger depth circuits.
Jan Johannsen
CC BY-SA 3.0
2012-01-22T12:20:44.837Z
2012-01-23T19:23:16.303Z
2012-01-23T19:23:16.303Z
Juho
<p>the major std/known solution to CNF minimization in EE is the <a href="http://en.wikipedia.org/wiki/Quine%E2%80%93McCluskey_algorithm">Quine-McCluskey algorithm</a> which there are many implementations, some public domain. however my understanding is that (not mentioned in the current wikipedia article) most revert to heuristics and greedy algorithms to find solutions esp for large formulas, ie they dont nec. find the optimal solution esp. for large input instances. </p>

<p>Quine-MCluskey is a generalization of working with Karnough maps which diagrams can succeed for small instances.</p>

<p>and note that there can be multiple optimal solutions in terms of equivalent formulas with the same (minimal) clause size, this will be pointed out in a good reference on the subj. finding the minimum apparently reduces to listing all prime implicates which can involve a massive exponential blowup in memory/"space" compared to the size of the original formula.</p>

CC BY-SA 3.0
2012-01-22T16:32:05.783Z
2012-01-22T16:32:05.783Z
vzn
<p>The problem of determining whether there is an equivalent CNF formula with at most a given number of literals is $\Pi_2^p$-complete.  The version minimizing the number of clauses is within a factor of $n$ of the formula size, where $n$ is the number of variables.  See section 6 of:</p>

<ul>
<li>Christopher Umans, <em>The Minimum Equivalent DNF Problem and Shortest Implicants</em>, JCSS <strong>63</strong>(4), 597–611, 2001.  doi:<a href="http://dx.doi.org/10.1006/jcss.2001.1775">10.1006/jcss.2001.1775</a> (<a href="http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.38.2930&amp;rep=rep1&amp;type=pdf">preprint</a>)</li>
</ul>

<p>A recent result shows that computing a particular lower bound for the size of the shortest equivalent CNF formula (measured by number of clauses, as you specify) is NP-complete.  This paper also states that your problem of minimizing the number of clauses is $\Pi^p_2$-complete as well, citing the Umans paper above, although why this follows is not immediately obvious to me.</p>

<ul>
<li>Ondřej Čepek, Petr Kučera and Petr Savický, <em>Boolean functions with a simple certificate for CNF complexity</em>, DAM <strong>160</strong>(4–5), 365–382, 2012.  doi:<a href="http://dx.doi.org/10.1016/j.dam.2011.05.013">10.1016/j.dam.2011.05.013</a> </li>
</ul>

CC BY-SA 3.0
2012-01-25T19:57:59.377Z
2012-01-25T19:57:59.377Z
András Salamon
<p>Let $F_1$ be a <strong>satisfiable</strong> CNF Formula with $n$ variables and $m$ clauses. Let $S_{F_1}$ be the solution space of $F_1$.</p>

<p>Consider the problem of determining, given $F_1$, another CNF Formula $F_2$ with the same set of variables as $F_1$, with $S_{F_2} = S_{F_1}$ (same solution space as $F_1$), but with as few clauses as possible (the only aim is to minimize the number of clauses, so how many literals each clause may have is not relevant).</p>

<blockquote>
  <p><strong>Question</strong>  </p>
  
  <p>Did anyone already investigated this problem? Are there any results in the literature concerning it?</p>
</blockquote>

<p>As an example, consider the following CNF Formula $F_1$ (each row is a clause):  </p>

<p>$x_1 \lor x_2 \lor x_3$<br>
$x_2 \lor x_3 \lor x_4$<br>
$\lnot x_1 \lor x_2 \lor x_4$<br>
$\lnot x_1 \lor x_2 \lor \lnot x_3$<br>
$\lnot x_1 \lor x_3 \lor x_5$<br>
$\lnot x_1 \lor x_2 \lor \lnot x_5$  </p>

<p>and the following formula $F_2$:  </p>

<p>$x_1 \lor x_2 \lor x_3$<br>
$x_2 \lor x_3 \lor x_4$<br>
$\lnot x_1 \lor x_3 \lor x_5$<br>
$\lnot x_1 \lor x_2$  </p>

<p>both have the same solution space, but while $F_1$ has $6$ clauses, $F_2$ only has $4$.  </p>

<p>Finally, consider the following formula $F_3$:  </p>

<p>$x_2 \lor x_3$<br>
$\lnot x_1 \lor x_3 \lor x_5$<br>
$\lnot x_1 \lor x_2$  </p>

<p>The solution space is again the same, but with only $3$ clauses.</p>

CC BY-SA 3.0
2012-01-21T14:17:59.277Z
What do you mean by set being “small”?  Do you want to minimize the number of clauses, or something else?
Tsuyoshi Ito
CC BY-SA 3.0
2012-01-21T14:47:24.500Z
@tsuyoshi I think he wants to get a cnf formula that is made up of minimum number of clauses with same solution space
Tayfun Pay
CC BY-SA 3.0
2012-01-21T15:57:28.710Z
@TsuyoshiIto: Yes, I want to minimize the number of clauses. I pose no restriction on the number of literals each clause may have.
Giorgio Camerani
CC BY-SA 3.0
2012-01-21T16:02:08.130Z
I asked this because the meaning of “small” in the question is ambiguous.  (Another common meaning in this context is to minimize the sum of the lengths of clauses.)  Please edit the question so that people do not have to read the comments to understand the question.
Tsuyoshi Ito
CC BY-SA 3.0
2012-01-21T19:39:44.030Z
this is a common problem in electrical engineering/circuit design ie CNF minimization. using a greedy algorithm part of the resulting minimization problem reduces to the NP complete minimum set cover. if you look up "karnough maps" via google (which are used for very small examples) you can find much related info.
vzn
CC BY-SA 3.0
2012-01-21T19:42:48.393Z
unfortunately think there can be multiple "minimal" forms measured by number of clauses ie in some cases two equivalent "smallest" formulas with same # of clauses. also believe that the minimization problem has been proven significantly harder than NP complete (not surprising)
vzn
CC BY-SA 3.0
2012-01-22T18:30:58.747Z
For any reasonable definition of "small", the problem is NP-hard.  A CNF formula is satisfiable if and only if it is *not* equivalent to the formula "False", which has zero clauses.
Jeffε
CC BY-SA 3.0
2012-01-22T19:26:32.790Z
@JɛﬀE: The formula "False" has $1$ clause, with $0$ literals (i.e. the __empty__ clause, which represents the disjunction of no possibilities). On the other hand, a formula with $0$ clauses is a tautology.
Giorgio Camerani
CC BY-SA 3.0
2012-01-22T20:00:22.637Z
Section 6 of http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.38.2930&rep=rep1&type=pdf mentions that the problem of determining whether there is an equivalent CNF formula with at most a given number of literals is $\Pi_2^p$-complete.  I'm not sure I understand why your version minimizing the number of clauses is interesting, as this is within a factor of $n$ of the formula size, where $n$ is the number of variables.
András Salamon
CC BY-SA 3.0
2012-01-22T22:26:55.027Z
Also, another recent result is of relevance: http://dx.doi.org/10.1016/j.dam.2011.05.013
András Salamon
CC BY-SA 3.0
2012-01-23T19:53:53.107Z
@AndrásSalamon: Why don't you turn your $3$ comments into an answer?
Giorgio Camerani
<cc.complexity-theory><co.combinatorics><sat><formulas>
Shortest Equivalent CNF Formula
Giorgio Camerani
# Shortest Equivalent CNF Formula

(Asked by: username_0 on 2012-01-21)

Let $F\_1$ be a **satisfiable** CNF Formula with $n$ variables and $m$ clauses. Let $S\_{F\_1}$ be the solution space of $F\_1$.

Consider the problem of determining, given $F\_1$, another CNF Formula $F\_2$ with the same set of variables as $F\_1$, with $S\_{F\_2} = S\_{F\_1}$ (same solution space as $F\_1$), but with as few clauses as possible (the only aim is to minimize the number of clauses, so how many literals each clause may have is not relevant).

> **Question**
>
> Did anyone already investigated this problem? Are there any results in the literature concerning it?

As an example, consider the following CNF Formula $F\_1$ (each row is a clause):

$x\_1 \lor x\_2 \lor x\_3$  
$x\_2 \lor x\_3 \lor x\_4$  
$\lnot x\_1 \lor x\_2 \lor x\_4$  
$\lnot x\_1 \lor x\_2 \lor \lnot x\_3$  
$\lnot x\_1 \lor x\_3 \lor x\_5$  
$\lnot x\_1 \lor x\_2 \lor \lnot x\_5$

and the following formula $F\_2$:

$x\_1 \lor x\_2 \lor x\_3$  
$x\_2 \lor x\_3 \lor x\_4$  
$\lnot x\_1 \lor x\_3 \lor x\_5$  
$\lnot x\_1 \lor x\_2$

both have the same solution space, but while $F\_1$ has $6$ clauses, $F\_2$ only has $4$.

Finally, consider the following formula $F\_3$:

$x\_2 \lor x\_3$  
$\lnot x\_1 \lor x\_3 \lor x\_5$  
$\lnot x\_1 \lor x\_2$

The solution space is again the same, but with only $3$ clauses.

**Tags:** cc.complexity-theory, co.combinatorics, sat, formulas
> **Comments:**
> **username_1**: What do you mean by set being “small”?  Do you want to minimize the number of clauses, or something else?  
> **username_2**: @tsuyoshi I think he wants to get a cnf formula that is made up of minimum number of clauses with same solution space  
> **username_0**: @TsuyoshiIto: Yes, I want to minimize the number of clauses. I pose no restriction on the number of literals each clause may have.  
> **username_1**: I asked this because the meaning of “small” in the question is ambiguous.  (Another common meaning in this context is to minimize the sum of the lengths of clauses.)  Please edit the question so that people do not have to read the comments to understand the question.  
> **username_3**: this is a common problem in electrical engineering/circuit design ie CNF minimization. using a greedy algorithm part of the resulting minimization problem reduces to the NP complete minimum set cover. if you look up "karnough maps" via google (which are used for very small examples) you can find much related info.  
> **username_3**: unfortunately think there can be multiple "minimal" forms measured by number of clauses ie in some cases two equivalent "smallest" formulas with same # of clauses. also believe that the minimization problem has been proven significantly harder than NP complete (not surprising)  
> **username_4**: For any reasonable definition of "small", the problem is NP-hard.  A CNF formula is satisfiable if and only if it is *not* equivalent to the formula "False", which has zero clauses.  
> **username_0**: @JɛﬀE: The formula "False" has $1$ clause, with $0$ literals (i.e. the __empty__ clause, which represents the disjunction of no possibilities). On the other hand, a formula with $0$ clauses is a tautology.  
> **username_5**: Section 6 of http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.38.2930&rep=rep1&type=pdf mentions that the problem of determining whether there is an equivalent CNF formula with at most a given number of literals is $\Pi_2^p$-complete.  I'm not sure I understand why your version minimizing the number of clauses is interesting, as this is within a factor of $n$ of the formula size, where $n$ is the number of variables.  
> **username_5**: Also, another recent result is of relevance: http://dx.doi.org/10.1016/j.dam.2011.05.013  
> **username_0**: @AndrásSalamon: Why don't you turn your $3$ comments into an answer?  

---

## 3 answers

### Answer by username_5 on 2012-01-25. Score: 11 | Accepted answer

The problem of determining whether there is an equivalent CNF formula with at most a given number of literals is $\Pi\_2^p$-complete. The version minimizing the number of clauses is within a factor of $n$ of the formula size, where $n$ is the number of variables. See section 6 of:

* Christopher Umans, *The Minimum Equivalent DNF Problem and Shortest Implicants*, JCSS **63**(4), 597–611, 2001. doi:[10.1006/jcss.2001.1775](http://dx.doi.org/10.1006/jcss.2001.1775) ([preprint](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.38.2930&rep=rep1&type=pdf))

A recent result shows that computing a particular lower bound for the size of the shortest equivalent CNF formula (measured by number of clauses, as you specify) is NP-complete. This paper also states that your problem of minimizing the number of clauses is $\Pi^p\_2$-complete as well, citing the Umans paper above, although why this follows is not immediately obvious to me.

* Ondřej Čepek, Petr Kučera and Petr Savický, *Boolean functions with a simple certificate for CNF complexity*, DAM **160**(4–5), 365–382, 2012. doi:[10.1016/j.dam.2011.05.013](http://dx.doi.org/10.1016/j.dam.2011.05.013)


---

### Answer by username_6 on 2012-01-22. Score: 9

The [circuit minization problem](http://en.wikipedia.org/wiki/Circuit_minimization) is intractable (see the comments below). Also what I think you might be interested in is the technique some SAT solvers apply (at least to some degree) that is called SAT preprocessing. For example the well known MiniSAT solver uses a [CNF minimizer SatELite](http://minisat.se/downloads/SatELite.pdf) to preprocess an instance. Google Scholar gives a lot of results for "sat preprocessing" as well.

> **Comments:**
> **username_5**: I thought Buchfuhrer and Umans in 2008 settled the circuit minimization problem being $\Pi^p_2$-complete, under Turing reductions?  
> **username_7**: Umans already showed in 1998 that finding a minimum equivalent CNF formula is $\Sigma^P_2$-hard (http://dx.doi.org/10.1006/jcss.2001.1775 ). The paper András mentions generalizes this to larger depth circuits.  

---

### Answer by username_3 on 2012-01-22. Score: 7

the major std/known solution to CNF minimization in EE is the [Quine-McCluskey algorithm](http://en.wikipedia.org/wiki/Quine%E2%80%93McCluskey_algorithm) which there are many implementations, some public domain. however my understanding is that (not mentioned in the current wikipedia article) most revert to heuristics and greedy algorithms to find solutions esp for large formulas, ie they dont nec. find the optimal solution esp. for large input instances.

Quine-MCluskey is a generalization of working with Karnough maps which diagrams can succeed for small instances.

and note that there can be multiple optimal solutions in terms of equivalent formulas with the same (minimal) clause size, this will be pointed out in a good reference on the subj. finding the minimum apparently reduces to listing all prime implicates which can involve a massive exponential blowup in memory/"space" compared to the size of the original formula.


---

