19
$\begingroup$

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.

Improve this question
$\endgroup$
11
  • 2
    $\begingroup$ @tsuyoshi I think he wants to get a cnf formula that is made up of minimum number of clauses with same solution space $\endgroup$
    – Tayfun Pay
    Commented Jan 21, 2012 at 14:47
  • 1
    $\begingroup$ @TsuyoshiIto: Yes, I want to minimize the number of clauses. I pose no restriction on the number of literals each clause may have. $\endgroup$
    – Giorgio Camerani
    Commented Jan 21, 2012 at 15:57
  • 2
    $\begingroup$ 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. $\endgroup$
    – Jeffε
    Commented Jan 22, 2012 at 18:30
  • 1
    $\begingroup$ 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. $\endgroup$
    – András Salamon
    Commented Jan 22, 2012 at 20:00
  • 1
    $\begingroup$ Also, another recent result is of relevance: dx.doi.org/10.1016/j.dam.2011.05.013 $\endgroup$
    – András Salamon
    Commented Jan 22, 2012 at 22:26

3 Answers 3

Reset to default
11
$\begingroup$

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
Improve this answer
$\endgroup$
9
$\begingroup$

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.

Improve this answer
$\endgroup$
2
  • 2
    $\begingroup$ I thought Buchfuhrer and Umans in 2008 settled the circuit minimization problem being $\Pi^p_2$-complete, under Turing reductions? $\endgroup$
    – András Salamon
    Commented Jan 22, 2012 at 21:56
  • 1
    $\begingroup$ 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. $\endgroup$
    – Jan Johannsen
    Commented Jan 23, 2012 at 10:10
7
$\begingroup$

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.

Improve this answer
$\endgroup$

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.