Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On complexity of restricted fragments of Decision DNNF

Andrea Calí, Igor Razgon

TL;DR

The paper advances understanding of the representation complexity for restricted fragments of Decision DNNF, notably $\wedge_d$-OBDDs, by introducing a generic lower-bound methodology, re-deriving XP bounds, and proving exponential separations among fbdd, $\wedge_d$-OBDD, and OBDD. It further proposes Structured $\wedge_d$-FBDD, showing it achieves FPT representations for CNFs that become bounded primal width after removing a constant number of clauses, while identifying inherent XP limits for other models via long clauses. These results illuminate the trade-offs between component analysis and fixed variable orderings in knowledge compilation and have implications for SAT solvers and proof complexity. The work also lays groundwork for future exploration of structured and weakly structured variants, aiming to bridge gaps toward broader FPT representations for CNFs of bounded width.

Abstract

Decision DNNF (a.k.a. $\wedge_d$-FBDD) is an important special case of Decomposable Negation Normal Form (DNNF). Decision DNNF admits FPT sized representation of CNFs of bounded \emph{primal} treewidth. However, the complexity of representation for CNFs of bounded \emph{incidence} treewidth is wide open. In the main part of this paper we carry out an in-depth study of the $\wedge_d$-OBDD model. We formulate a generic methodology for proving lower bounds for the model. Using this methodology, we reestablish the XP lower bound provided in [arxiv:1708.07767]. We also provide exponential separations between FBDD and $\wedge_d$-OBDD and between $\wedge_d$-OBDD and an ordinary OBDD. The last separation is somewhat surprising since $\wedge_d$-FBDD can be quasipolynomially simulated by FBDD. In the remaining part of the paper, we introduce a relaxed version of Structured Decision DNNF that we name Structured $\wedge_d$-FBDD. We demonstrate that this model is quite powerful for CNFs of bounded incidence treewidth: it has an FPT representation for CNFs that can be turned into ones of bounded primal treewidth by removal of a constant number of clauses (while for both $\wedge_d$-OBDD and Structured Decision DNNF an XP lower bound is triggered by just two long clauses).

On complexity of restricted fragments of Decision DNNF

TL;DR

The paper advances understanding of the representation complexity for restricted fragments of Decision DNNF, notably -OBDDs, by introducing a generic lower-bound methodology, re-deriving XP bounds, and proving exponential separations among fbdd, -OBDD, and OBDD. It further proposes Structured -FBDD, showing it achieves FPT representations for CNFs that become bounded primal width after removing a constant number of clauses, while identifying inherent XP limits for other models via long clauses. These results illuminate the trade-offs between component analysis and fixed variable orderings in knowledge compilation and have implications for SAT solvers and proof complexity. The work also lays groundwork for future exploration of structured and weakly structured variants, aiming to bridge gaps toward broader FPT representations for CNFs of bounded width.

Abstract

Decision DNNF (a.k.a. -FBDD) is an important special case of Decomposable Negation Normal Form (DNNF). Decision DNNF admits FPT sized representation of CNFs of bounded \emph{primal} treewidth. However, the complexity of representation for CNFs of bounded \emph{incidence} treewidth is wide open. In the main part of this paper we carry out an in-depth study of the -OBDD model. We formulate a generic methodology for proving lower bounds for the model. Using this methodology, we reestablish the XP lower bound provided in [arxiv:1708.07767]. We also provide exponential separations between FBDD and -OBDD and between -OBDD and an ordinary OBDD. The last separation is somewhat surprising since -FBDD can be quasipolynomially simulated by FBDD. In the remaining part of the paper, we introduce a relaxed version of Structured Decision DNNF that we name Structured -FBDD. We demonstrate that this model is quite powerful for CNFs of bounded incidence treewidth: it has an FPT representation for CNFs that can be turned into ones of bounded primal treewidth by removal of a constant number of clauses (while for both -OBDD and Structured Decision DNNF an XP lower bound is triggered by just two long clauses).
Paper Structure (16 sections, 31 theorems, 6 equations, 1 figure)

This paper contains 16 sections, 31 theorems, 6 equations, 1 figure.

Table of Contents

  1. Introduction
  2. The main objective
  3. Motivation
  4. Our results and structure of the paper
  5. Preliminaries
  6. Assignments, rectangles, Boolean functions
  7. Models of Boolean functions
  8. Graphs, width parameters, and correspondence with cnf
  9. $\wedge_d$-obdd: incidence treewidth inefficiency and separations
  10. An approach to proving $\wedge_d$-obbd lower bounds
  11. $\wedge_d$-obdd lower bounds and separations
  12. Proofs of Theorem \ref{['obddengine1']} and \ref{['obddengine2']}
  13. The effect of structuredness on Decision dnnf
  14. Conclusion
  15. Proof of Lemma \ref{['lem:restr1']}
  16. ...and 1 more sections

Key Result

Proposition 1

Suppose that $\mathcal{H}=\prod_{i \in [m]} \mathcal{H}_i$, $m \geq 2$ and $\mathcal{H}_i$ is uniform for each $i \in [m]$. Further on, assume that $\mathcal{H}$ is not a rectangle breaking a set $Y \subseteq \mathsf{var}(\mathcal{H})$ Then there is $i \in [m]$ such that $Y \subseteq \mathsf{var}(\m

Figures (1)

  • Figure 1: A $\wedge_d$-obdd and its alignment

Theorems & Definitions (95)

  • Definition 1
  • Proposition 1
  • Definition 2
  • Definition 3
  • Definition 4
  • Definition 5
  • Definition 6
  • Remark 1
  • Example 1
  • Definition 7
  • ...and 85 more