Shortest Equivalent CNF Formula

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.

• @tsuyoshi I think he wants to get a cnf formula that is made up of minimum number of clauses with same solution space Jan 21 '12 at 14:47
• @TsuyoshiIto: Yes, I want to minimize the number of clauses. I pose no restriction on the number of literals each clause may have. Jan 21 '12 at 15:57
• 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. Jan 22 '12 at 18:30
• Section 6 of citeseerx.ist.psu.edu/viewdoc/… 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. Jan 22 '12 at 20:00
• Also, another recent result is of relevance: dx.doi.org/10.1016/j.dam.2011.05.013 Jan 22 '12 at 22:26

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:

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

The circuit minization problem 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 to preprocess an instance. Google Scholar gives a lot of results for "sat preprocessing" as well.

• I thought Buchfuhrer and Umans in 2008 settled the circuit minimization problem being $\Pi^p_2$-complete, under Turing reductions? Jan 22 '12 at 21:56
• Umans already showed in 1998 that finding a minimum equivalent CNF formula is $\Sigma^P_2$-hard (dx.doi.org/10.1006/jcss.2001.1775 ). The paper András mentions generalizes this to larger depth circuits. Jan 23 '12 at 10:10

the major std/known solution to CNF minimization in EE is the Quine-McCluskey 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.