Lower Bounds on Intermediate Results in Bottom-Up Knowledge Compilation
Alexis de Colnet, Stefan Mengel
摘要
Bottom-up knowledge compilation is a paradigm for generating representations of functions by iteratively conjoining constraints using a so-called apply function. When the input is not efficiently compilable into a language - generally a class of circuits - because optimal compiled representations are provably large, the problem is not the compilation algorithm as much as the choice of a language too restrictive for the input. In contrast, in this paper, we look at CNF formulas for which very small circuits exists and look at the efficiency of their bottom-up compilation in one of the most general languages, namely that of structured decomposable negation normal forms (str-DNNF). We prove that, while the inputs have constant size representations as str-DNNF, any bottom-up compilation in the general setting where conjunction and structure modification are allowed takes exponential time and space, since large intermediate results have to be produced. This unconditionally proves that the inefficiency of bottom-up compilation resides in the bottom-up paradigm itself.
问问这篇 Paper
智能体会读完全文。
Lune 把这篇 Paper 索引到了每一个公式,引用它的顶会 Paper 也一样。你提问,回答直接引用原文。
相关 Paper
- A Compiler for Weak Decomposable Negation Normal FormPetr Illner, Petr KuceraAAAI 2024
- Backdoor Decomposable Monotone Circuits and Propagation Complete EncodingsPetr Kucera, Petr SavickýAAAI 2021 · 被引用 1 次
- An And-Sum Circuit with Signed Edges That Is More Succinct than SDDRyoma Onaka, Kengo Nakamura, Masaaki Nishino, Norihito YasudaAAAI 2025 · 被引用 2 次
- Certifying Top-Down Decision-DNNF CompilersFlorent Capelli, Jean-Marie Lagniez, Pierre MarquisAAAI 2021 · 被引用 9 次
- Counterexample Guided Knowledge Compilation for Boolean Functional SynthesisS. Akshay, Supratik Chakraborty, Sahil JainCAV 2023
