0
$\begingroup$

I am reading the naive conversion to CNF, this procedure is explaining in this book book, but I have not found a conplexity analysis of this algorithm:

  1. elimination of equivalence
  2. Elimination of Implications
  3. elimination of double negation
  4. De Morgan Laws
  5. distributive law

I found one implementation of this method in this Repo https://github.com/netom/satispy

Thanks

$\endgroup$
  • 2
    $\begingroup$ Can you summarize the algorithm in the question, to make your question self-contained, so we don't have to read external links or read a book to understand the question? What are your thoughts? Are there any steps where you do know what the complexity will be? $\endgroup$ – D.W. Sep 2 at 16:15
  • $\begingroup$ I found one implementation of this method in this Repo github.com/netom/satispy $\endgroup$ – dimitruss Sep 2 at 16:29
  • $\begingroup$ Sorry, that's still an external link, so it doesn't address my comment. Trying to read someone else's code that implements an algorithm is often a miserable way to understand what the algorithm is doing. $\endgroup$ – D.W. Sep 2 at 16:31
  • $\begingroup$ I would think that this question is answered in sufficient depth in Sisper's book, assuming you can relate your textbook algorithm to what's discussed in Sipser's book. The two answers given so far show exactly where the difference is: weakening the requirements for the conversion algorithm from equivalence to equisatisfiability is a sufficient step to overcome the otherwise exponential hardness of the problem. $\endgroup$ – Kai Oct 15 at 12:15
1
$\begingroup$

Any algorithm necessarily has exponential complexity, since the CNF of a formula can be exponentially longer than the DNF, and the input might be in DNF.

$\endgroup$
0
$\begingroup$

If you require a logically equivalent CNF formula, then that will give you a worst-case exponential size formula.

If, however, equisatisfiability is enough, then you can use Tseitin encoding, which will give you a polynomial size formula. The trick is in adding new atoms for logical operators.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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