A Strongly Exponential Separation of DNNFs from CNF Formulas

TL;DR

This paper establishes a strongly exponential lower bound on the size of DNNFs for certain CNF formulas, demonstrating a significant separation between DNNFs and CNF formulas in prime implicates form, resolving an open problem in knowledge compilation.

Contribution

It proves a strongly exponential lower bound on DNNF size for CNF formulas from expander graphs, showing a fundamental separation in knowledge compilation.

Findings

Exponential lower bound on DNNF size for specific CNF formulas

Strong separation between DNNFs and CNF prime implicates

Resolution of an open problem in knowledge compilation

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).