Pith. sign in

REVIEW 4 cited by

A Strongly Exponential Separation of DNNFs from CNF Formulas

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 1411.1995 v3 pith:MD342BVC submitted 2014-11-07 cs.CC

Simone Bova , Florent Capelli , Stefan Mengel , Friedrich Slivovsky This is my paper · ORCID
classification cs.CC
keywords dnnfsexponentialformulasstronglyformnegationnormalseparation
verification ladder T0 review T1 audit T2 compute T3 formal

Signed reviews

No signed human review yet.

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

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 4 Pith papers

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

  1. Proof Systems Based on Structured Circuits

    cs.CC 2026-05 unverdicted novelty 7.0 of 10

    SDDs and d-SDNNFs yield strictly smaller refutations than OBDDs for unsatisfiable CNFs, with separations under different derivation rules and a sat-to-unsat lifting theorem.

  2. Compilation and Fast Model Counting beyond CNF

    cs.CC 2025-02 conditional novelty 7.0 of 10

    Conjunctions of constant-width OBDD-representable constraints can be compiled into d-DNNF circuits in fixed-parameter tractable time when parameterized by incidence treewidth.

  3. A Distributed Framework for Compiling and Reasoning with d-DNNF

    cs.DC 2026-07 conditional novelty 6.0 of 10

    A Cube-and-Conquer framework compiles CNF formulas into a virtual d-DNNF distributed across workers, enabling counting, direct access, and uniform sampling under conditioning.

  4. Decision DNNFs with imbalanced conjunction cannot efficiently represent CNFs of bounded width

    cs.CC 2025-05 conditional novelty 6.0 of 10

    For CNFs that encode a ternary tree crossed with a path, Decision DNNFs whose conjunction gates split variables imbalancedly require size at least n^{Ω((1−α)√k)}, ruling out FPT-sized representations.

Pith tools