Compilation and Fast Model Counting beyond CNF

• URL: http://arxiv.org/abs/2502.00434v1
• Date: Sat, 01 Feb 2025 14:00:04 GMT
• Title: Compilation and Fast Model Counting beyond CNF
• Authors: Alexis de Colnet, Stefan Szeider, Tianwei Zhang,
• Abstract summary: 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.
• Score: 31.620928650659586
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Presburger Functional Synthesis: Complexity and Tractable Normal Forms [0.4499833362998487]
  We show that Presburger Functional Synthesis (PFnS) can be solved in EXPTIME and provide a matching exponential lower bound.<n>We then identify a special normal form, called PSyNF, for the specification formula that guarantees poly-time and poly-size solvability of PFnS.<n>We prove several properties of PSyNF, including how to check and compile to this form, and conditions under which any other form that guarantees poly-time solvability of PFnS can be compiled in poly-time to PSyNF.
  arXiv  Detail & Related papers  (2025-08-10T07:00:34Z)
• Pseudo-Boolean d-DNNF Compilation for Expressive Feature Modeling Constructs [2.4497587364567925]
  We provide a pseudo-Boolean encoding for feature models, which facilitates smaller representations of commonly employed constructs.<n>We also propose a novel method to compile pseudo-Boolean formulas to Boolean d-DNNF.
  arXiv  Detail & Related papers  (2025-05-09T12:00:43Z)
• The Limits of Tractable Marginalization [23.716205079188608]
  Marginalization -- summing a function over all assignments to a subset of its inputs -- is a fundamental computational problem.<n>We show that when there is an efficient real RAM performing virtual evidence marginalization for a function, then there are small circuits for that function's multilinear representation.<n>We conclude with a result, showing that whenever there is an efficient real RAM performing virtual evidence marginalization for a function, then there are small circuits for that function's multilinear representation.
  arXiv  Detail & Related papers  (2025-04-17T07:54:56Z)
• 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)
• Tractable Bounding of Counterfactual Queries by Knowledge Compilation [51.47174989680976]
  We discuss the problem of bounding partially identifiable queries, such as counterfactuals, in Pearlian structural causal models. A recently proposed iterated EM scheme yields an inner approximation of those bounds by sampling the initialisation parameters. We show how a single symbolic knowledge compilation allows us to obtain the circuit structure with symbolic parameters to be replaced by their actual values.
  arXiv  Detail & Related papers  (2023-10-05T07:10:40Z)
• 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)
• Synthesising Recursive Functions for First-Order Model Counting: Challenges, Progress, and Conjectures [12.47276164048813]
  First-order model counting (FOMC) is a computational problem that asks to count the models of a sentence in finite-domain first-order logic. We relax the restrictions that typically accompany domain recursion to work with directed graphs that may contain cycles. These improvements allow the algorithm to find efficient solutions to counting problems that were previously beyond its reach.
  arXiv  Detail & Related papers  (2023-06-07T06:49:01Z)
• Bayesian Kernelized Tensor Factorization as Surrogate for Bayesian Optimization [13.896697187967545]
  Kernel optimization (BO) primarily uses Gaussian processes (GP) as the key surrogate model. In this paper, we propose to use Bayesian Factorization (BKTF) as a new surrogate model -- for BO in a $D$-dimensional product space. BKTF offers a flexible and highly effective approach for characterizing complex functions with uncertainty quantification.
  arXiv  Detail & Related papers  (2023-02-28T12:00:21Z)
• 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)
• Exponentially Weighted l_2 Regularization Strategy in Constructing Reinforced Second-order Fuzzy Rule-based Model [72.57056258027336]
  In the conventional Takagi-Sugeno-Kang (TSK)-type fuzzy models, constant or linear functions are usually utilized as the consequent parts of the fuzzy rules. We introduce an exponential weight approach inspired by the weight function theory encountered in harmonic analysis.
  arXiv  Detail & Related papers  (2020-07-02T15:42:15Z)
• 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)
• Polynomial-Time Exact MAP Inference on Discrete Models with Global Dependencies [83.05591911173332]
  junction tree algorithm is the most general solution for exact MAP inference with run-time guarantees. We propose a new graph transformation technique via node cloning which ensures a run-time for solving our target problem independently of the form of a corresponding clique tree.
  arXiv  Detail & Related papers  (2019-12-27T13:30:29Z)
• Learning Likelihoods with Conditional Normalizing Flows [54.60456010771409]
  Conditional normalizing flows (CNFs) are efficient in sampling and inference. We present a study of CNFs where the base density to output space mapping is conditioned on an input x, to model conditional densities p(y|x)
  arXiv  Detail & Related papers  (2019-11-29T19:17:58Z)

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.