Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Compilation and Fast Model Counting beyond CNF

Alexis de Colnet, Stefan Szeider, Tianwei Zhang

TL;DR

We address the problem of efficiently counting models for systems of Boolean constraints beyond CNF by leveraging incidence treewidth. The authors introduce the notion of $w$-slim constraints for complete OBDDs/SDNNFs and prove a fixed-parameter tractable compilation to d-SDNNF for conjunctions of such constraints, with running time $2^{O(k)}\mathrm{poly}(|F|+|\mathrm{var}(F)|)$ where $k=\mathrm{tw}_i(F)$. A central technique is encoding each constraint via Tseitin CNF with auxiliary variables, constructing per-constraint vtrees, and then merging these encodings to bound the incidence width and enable FPT compilation; a complementary approach yields faster model counting for a subfamily without compilation. The paper also provides lower bounds showing the exponent cannot be removed and presents a faster DP-based model counting scheme for one-sided and modulo constraints, demonstrating practical advantages for parity, cardinality, and threshold-like constraints. Overall, the work broadens the reach of knowledge compilation beyond CNF, offering both theoretical insights and practical counting methods for a wide class of constraints.

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.

Compilation and Fast Model Counting beyond CNF

TL;DR

We address the problem of efficiently counting models for systems of Boolean constraints beyond CNF by leveraging incidence treewidth. The authors introduce the notion of -slim constraints for complete OBDDs/SDNNFs and prove a fixed-parameter tractable compilation to d-SDNNF for conjunctions of such constraints, with running time where . A central technique is encoding each constraint via Tseitin CNF with auxiliary variables, constructing per-constraint vtrees, and then merging these encodings to bound the incidence width and enable FPT compilation; a complementary approach yields faster model counting for a subfamily without compilation. The paper also provides lower bounds showing the exponent cannot be removed and presents a faster DP-based model counting scheme for one-sided and modulo constraints, demonstrating practical advantages for parity, cardinality, and threshold-like constraints. Overall, the work broadens the reach of knowledge compilation beyond CNF, offering both theoretical insights and practical counting methods for a wide class of constraints.

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.

Paper Structure

This paper contains 22 sections, 36 theorems, 23 equations, 4 figures, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Treewidth and Tree Decompositions
  4. OBDDs and SDNNF Circuits
  5. (d-)SDNNF Circuits.
  6. OBDDs.
  7. Width measures.
  8. Slim Functions and STS
  9. Slim Functions for Complete OBDDs and SDNNFs
  10. Commutative State Transitions Systems
  11. FPT Compilation of Systems of $O(1)$-Slim Constraints
  12. The Tseitin Encoding
  13. Proof of Theorem \ref{['theorem:main_fpt_compile']}
  14. Constructing the Vtrees
  15. Controlling the Treewidth of the Encoding
  16. ...and 7 more sections

Key Result

Theorem 1

Let $w$ be a constant integer and $\mathcal{C}$ be a class of constraints such that, for every $c \in \mathcal{C}$, and every subset $Y$ of $c$'s variables, at most $w$ different constraints can be obtained from $c$ by assigning variables in $Y$ in any way. There is an algorithm that, given a system

Figures (4)

  • Figure 1:
  • Figure 2: CSTS for XOR, OR and "$x_1 + \dots + x_n \geq 2$" constraints.
  • Figure 3:
  • Figure :

Theorems & Definitions (74)

  • Theorem 1
  • Theorem 2
  • Theorem 3: BovaCMS15
  • Definition 1
  • Definition 2
  • Lemma 1
  • proof
  • Claim 1
  • proof
  • Lemma 2
  • ...and 64 more