pith. machine review for the scientific record. sign in

arxiv: 1411.1995 · v3 · submitted 2014-11-07 · 💻 cs.CC

Recognition: unknown

A Strongly Exponential Separation of DNNFs from CNF Formulas

Simone Bova , Florent Capelli , Stefan Mengel , Friedrich Slivovsky
Authors on Pith no claims yet
classification 💻 cs.CC
keywords dnnfsexponentialformulasstronglyformnegationnormalseparation
0
0 comments X
read the original 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).

This paper has not been read by Pith yet.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Proof Systems Based on Structured Circuits

    cs.CC 2026-05 unverdicted novelty 7.0

    SDD- and d-SDNNF-based proof systems produce strictly smaller refutations than OBDD systems for unsatisfiable CNFs, with multiple separations under varying rules and a new sat-to-unsat lifting theorem.