A Strongly Exponential Separation of DNNFs from CNF Formulas
Computational Complexity
2015-02-20 v3
Abstract
Decomposable Negation Normal Forms (DNNFs) are Boolean circuits in negation normal form where the subcircuits leading into each AND gate are defined on disjoint sets of variables. We prove a strongly exponential lower bound on the size of DNNFs for a class of CNF formulas built from expander graphs. As a corollary, we obtain a strongly exponential separation between DNNFs and CNF formulas in prime implicates form. This settles an open problem in the area of knowledge compilation (Darwiche and Marquis, 2002).
Keywords
Cite
@article{arxiv.1411.1995,
title = {A Strongly Exponential Separation of DNNFs from CNF Formulas},
author = {Simone Bova and Florent Capelli and Stefan Mengel and Friedrich Slivovsky},
journal= {arXiv preprint arXiv:1411.1995},
year = {2015}
}