What is this?
The Knowledge Compilation Map is an interactive tool for exploring succinctness relations and tractability results across propositional language classes used in knowledge compilation. It is based on the foundational work of Darwiche & Marquis (2002) and incorporates results from subsequent research.
Languages
The map covers roughly 28 propositional language classes — including NNF, DNNF, d-DNNF, FBDD, OBDD, SDD, CNF, DNF, and others — organized in a directed graph where edges represent whether one language can be polynomially or quasi-polynomially compiled into another.
Operations
For each language, the map tracks support for standard queries (CO, VA, CE, IM, EQ, SE, CT, ME) and transformations (CD, FO, SFO, ∧C, ∧BC, ∨C, ∨BC, ¬C), indicating whether each can be performed in polynomial time, quasi-polynomial time, or not at all.
Automated reasoning
Starting from a hand-curated knowledge base of published results, the tool validates consistency and propagates derived facts through fixed-point algorithms:
- Upgrade propagation — transitive closure over succinctness edges infers new polynomial/quasi-polynomial compilations.
- Downgrade propagation — contradiction-based reasoning rules out compilations that would violate known negative results.
- Operation propagation — query and transformation support is inferred via succinctness relations and operation implication lemmas.
All derived entries are tagged with human-readable proof descriptions and literature references.
Separating functions
Exponential succinctness gaps between languages are witnessed by separating function families — Boolean functions like OR_n, Clique, Parity, and others — that have compact representations in one language but provably require exponential size in another.
Contributing
Know of a new result? Use the contribution workflow to propose new edges, operation results, or language additions. Submissions are reviewed before integration.