Deterministic DNNF Is Not Polynomially Closed Under Negation

Read the paper (PDF). This repository formalizes the proof that d-DNNF is not polynomially closed under negation and its circuit, grammar, and automaton corollaries.

Start with the formal statement, follow the proof modules, or browse the corollaries. The exponential separation strengthens the quasipolynomial gap in the paper to a linear-size d-DNNF whose negation requires exponential DNNF size.

With elan installed, run:

lake exe cache get
lake build DDNNFNegation DDNNFNegationCorollaries DDNNFNegationTests DDNNFNegationExponential
lake env lean scripts/Check.lean
lake env lean scripts/CheckCorollaries.lean
lake env lean scripts/CheckExponential.lean

Lean and Mathlib versions are pinned. CI builds the proof and corollaries and checks their axiom dependencies. Code: Apache 2.0.