Compilation and Fast Model Counting beyond CNF

TL;DR

This paper advances the understanding of efficient Boolean function compilation into d-DNNF by introducing fixed-parameter tractable methods for certain constraint classes, extending beyond traditional CNF representations.

Contribution

It presents the first fixed-parameter tractable compilation algorithms for conjunctions of constraints represented by constant-width OBDDs, broadening the scope beyond CNF.

Findings

FPT compilation is feasible for certain constraints with bounded incidence treewidth.

The approach includes parity and cardinality constraints with constant thresholds.

A more efficient FPT model counting algorithm is also proposed for specific constraint subclasses.

Abstract

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.