Compilation and Fast Model Counting beyond CNF
This work advances theoretical knowledge in computational logic and AI by enabling faster model counting for broader constraint classes, though it is incremental as it builds on existing CNF results.
The paper addresses the problem of efficiently compiling Boolean functions into d-DNNF for fast model counting, extending beyond CNF to include constraints like parity and cardinality with constant thresholds, achieving fixed-parameter tractable compilation parameterized by incidence treewidth.
Circuits in deterministic decomposable negation normal form (d-DNNF) are representations of Boolean functions that enable linear-time model counting. This paper strengthens our theoretical knowledge of what classes of functions can be efficiently transformed, or compiled, into d-DNNF. Our main contribution is the fixed-parameter tractable (FPT) compilation of conjunctions of specific constraints parameterized by incidence treewidth. This subsumes the known result for CNF. The constraints in question are all functions representable by constant-width ordered binary decision diagrams (OBDDs) for all variable orderings. For instance, this includes parity constraints and cardinality constraints with constant threshold. The running time of the FPT compilation is singly exponential in the incidence treewidth but hides large constants in the exponent. To balance that, we give a more efficient FPT algorithm for model counting that applies to a sub-family of the constraints and does not require compilation.