A canonical generalization of OBDD

• URL: http://arxiv.org/abs/2604.05537v1
• Date: Tue, 07 Apr 2026 07:36:21 GMT
• Title: A canonical generalization of OBDD
• Abstract summary: We introduce Tree Decision Diagrams (TDD) as a model for Boolean functions that generalizes OBDD.<n> TDDs enjoy the same tractability properties as OBDD, such as model counting, enumeration, conditioning, and apply, and are more succinct.<n>We show that CNF formulas of treewidth $k$ can be represented by TDDs of FPT size, which is known to be impossible for OBDD.
• Score: 30.681714489260898
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We introduce Tree Decision Diagrams (TDD) as a model for Boolean functions that generalizes OBDD. They can be seen as a restriction of structured d-DNNF; that is, d-DNNF that respect a vtree $T$. We show that TDDs enjoy the same tractability properties as OBDD, such as model counting, enumeration, conditioning, and apply, and are more succinct. In particular, we show that CNF formulas of treewidth $k$ can be represented by TDDs of FPT size, which is known to be impossible for OBDD. We study the complexity of compiling CNF formulas into deterministic TDDs via bottom-up compilation and relate the complexity of this approach with the notion of factor width introduced by Bova and Szeider.

Related papers

• Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs [48.390500145598544]
  Large language models (LLMs) have demonstrated significant potential in formal theorem proving.<n>We exploit an informative structure in formal verification: the observation that compilers map a vast space of diverse proof attempts.<n>We introduce a learning-to-refine framework that leverages this compression to perform efficient learning and proof exploration.
  arXiv  Detail & Related papers  (2026-03-13T01:33:20Z)
• Learning Decision Trees as Amortized Structure Inference [59.65621207449269]
  We propose a hybrid amortized structure inference approach to learn predictive decision tree ensembles given data.<n>We show that our approach, DT-GFN, outperforms state-of-the-art decision tree and deep learning methods on standard classification benchmarks.
  arXiv  Detail & Related papers  (2025-03-10T07:05:07Z)
• Compilation and Fast Model Counting beyond CNF [31.620928650659586]
  This paper strengthens our theoretical knowledge of what classes of functions can be efficiently transformed, or compiled, into d-DNNF.<n>The constraints in question are all functions representable by constant-width ordered binary decision diagrams (OBDDs) for all variable orderings.<n>We give a more efficient FPT algorithm for model counting that applies to a sub-family of the constraints and does not require compilation.
  arXiv  Detail & Related papers  (2025-02-01T14:00:04Z)
• Structural Entropy Guided Probabilistic Coding [52.01765333755793]
  We propose a novel structural entropy-guided probabilistic coding model, named SEPC.<n>We incorporate the relationship between latent variables into the optimization by proposing a structural entropy regularization loss.<n> Experimental results across 12 natural language understanding tasks, including both classification and regression tasks, demonstrate the superior performance of SEPC.
  arXiv  Detail & Related papers  (2024-12-12T00:37:53Z)
• Canonical Decision Diagrams Modulo Theories [0.19285000127136376]
  Decision diagrams are powerful tools to represent propositional formulas. Some forms of DDs (e.g., OBDDs, SDDs) are canonical, that is, (under given conditions on the atom list) they univocally represent equivalence classes of formulas. We present a novel technique to leverage DDs to SMT level, which has several advantages.
  arXiv  Detail & Related papers  (2024-04-25T09:34:49Z)
• Structured d-DNNF Is Not Closed Under Negation [0.0]
  Both structured d-DNNF and SDD can be exponentially more succinct than OBDD. We show that structured d-DNNF does not support polytime negation, disjunction, or existential operations. We also show that there are functions with an equivalent-sized structured d-DNNF but with no such representation as an SDD.
  arXiv  Detail & Related papers  (2024-02-07T13:31:59Z)
• Efficient Computation of Counterfactual Bounds [44.4263314637532]
  We compute exact counterfactual bounds via algorithms for credal nets on a subclass of structural causal models. We evaluate their accuracy by providing credible intervals on the quality of the approximation.
  arXiv  Detail & Related papers  (2023-07-17T07:59:47Z)
• DPO: Dynamic-Programming Optimization on Hybrid Constraints [26.704502486686128]
  In Bayesian inference, the most probable explanation (MPE) problem requests a variable instantiation with the highest probability given some evidence. It is known that Boolean MPE can be solved via reduction to (weighted partial) MaxSAT. We build on DPMC and introduce DPO, a dynamic-programming that exactly solves MPE.
  arXiv  Detail & Related papers  (2022-05-17T21:18:54Z)
• Belief Revision in Sentential Decision Diagrams [126.94029917018733]
  We develop a general revision algorithm for SDDs based on a syntactic characterisation of Dalal revision. Preliminary experiments performed with randomly generated knowledge bases show the advantages of directly perform revision within SDD formalism.
  arXiv  Detail & Related papers  (2022-01-20T11:01:41Z)
• Contextualized Semantic Distance between Highly Overlapped Texts [85.1541170468617]
  Overlapping frequently occurs in paired texts in natural language processing tasks like text editing and semantic similarity evaluation. This paper aims to address the issue with a mask-and-predict strategy. We take the words in the longest common sequence as neighboring words and use masked language modeling (MLM) to predict the distributions on their positions. Experiments on Semantic Textual Similarity show NDD to be more sensitive to various semantic differences, especially on highly overlapped paired texts.
  arXiv  Detail & Related papers  (2021-10-04T03:59:15Z)
• A Lower Bound on DNNF Encodings of Pseudo-Boolean Constraints [3.42658286826597]
  Two major considerations when encoding pseudo-Boolean constraints into SAT are the size of the encoding and its propagation strength. It has been shown that there exist PB-constraints whose ordered BDD (OBDD) representations, and thus the inferred CNF encodings, all have exponential size.
  arXiv  Detail & Related papers  (2021-01-06T10:25:22Z)
• Supervised Learning for Non-Sequential Data: A Canonical Polyadic Decomposition Approach [85.12934750565971]
  Efficient modelling of feature interactions underpins supervised learning for non-sequential tasks. To alleviate this issue, it has been proposed to implicitly represent the model parameters as a tensor. For enhanced expressiveness, we generalize the framework to allow feature mapping to arbitrarily high-dimensional feature vectors.
  arXiv  Detail & Related papers  (2020-01-27T22:38:40Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.