A Lower Bound on DNNF Encodings of Pseudo-Boolean Constraints

• URL: http://arxiv.org/abs/2101.01953v1
• Date: Wed, 6 Jan 2021 10:25:22 GMT
• Title: A Lower Bound on DNNF Encodings of Pseudo-Boolean Constraints
• Abstract summary: 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.
• Score: 3.42658286826597
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Two major considerations when encoding pseudo-Boolean (PB) constraints into SAT are the size of the encoding and its propagation strength, that is, the guarantee that it has a good behaviour under unit propagation. Several encodings with propagation strength guarantees rely upon prior compilation of the constraints into DNNF (decomposable negation normal form), BDD (binary decision diagram), or some other sub-variants. However it has been shown that there exist PB-constraints whose ordered BDD (OBDD) representations, and thus the inferred CNF encodings, all have exponential size. Since DNNFs are more succinct than OBDDs, preferring encodings via DNNF to avoid size explosion seems a legitimate choice. Yet in this paper, we prove the existence of PB-constraints whose DNNFs all require exponential size.

Related papers

• Constrained Decoding for Diffusion Language Models via Efficient Inference over Finite Automata [57.27430779838529]
  We present an exact and tractable algorithm for sampling from the constrained mean-field posterior under any constraint expressible as a finite automaton.<n>The approach guarantees constraint satisfaction by construction, supports both greedy and sampling-based decoding, and is compatible with parallel and block-wise decoding.<n> Empirical evaluations on Dream-7B and LLaDA-8 show substantial accuracy gains across various tasks.
  arXiv  Detail & Related papers  (2026-07-08T05:48:57Z)
• Truncated-Binary Encoding: Spectral Degree Reduction of Combinatorial Optimization Problems for Quantum Hardware [0.0]
  Exact-binary encoding compiles a discrete cost function network (CFN) into a higher-order unconstrained binary optimization (HUBO) problem.<n>We propose textittruncated-binary encoding (TBE): a modification of exact-binary encoding in which Ising-basis monomials exceeding a chosen cutoff $k_textmax$ are dropped from the encoded cost.
  arXiv  Detail & Related papers  (2026-05-16T20:27:06Z)
• A canonical generalization of OBDD [30.681714489260898]
  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.
  arXiv  Detail & Related papers  (2026-04-07T07:36:21Z)
• Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification [9.733843486234878]
  State-of-the-art neural network (NN) verifiers demonstrate that applying the branch-and-bound (BaB) procedure with fast bounding techniques plays a key role in tackling many challenging verification properties.<n>We introduce the linear constraint-driven clipping framework, a class of scalable and efficient methods designed to enhance the efficacy of NN verifiers.
  arXiv  Detail & Related papers  (2025-12-11T19:59:37Z)
• Scalable Verification of Neural Control Barrier Functions Using Linear Bound Propagation [50.53301323864253]
  Control barrier functions (CBFs) are a popular tool for safety certification of nonlinear dynamical control systems.<n>We present a novel framework for verifying neural CBFs based on piecewise linear upper and lower bounds on the conditions required for a neural network to be a CBF.<n>Our approach scales to larger neural networks than state-of-the-art verification procedures for CBFs.
  arXiv  Detail & Related papers  (2025-11-09T11:51:15Z)
• Toward Uncertainty-Aware and Generalizable Neural Decoding for Quantum LDPC Codes [0.9453554184019106]
  Quantum error correction (QEC) is essential for scalable quantum computing.<n>We propose textbfQuBA, a Bayesian graph neural decoder that integrates attention to both dot-product and multi-head.<n>We further develop textbfSAGU textbf(Sequential Aggregate Generalization under Uncertainty), a multi-code training framework with enhanced cross-domain robustness.
  arXiv  Detail & Related papers  (2025-10-05T01:08:39Z)
• 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. The constraints in question are all functions representable by constant-width ordered binary decision diagrams (OBDDs) for all variable orderings. 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)
• A shallow dive into the depths of non-termination checking for C programs [3.4144415576897624]
  Unintended Non-Termination (NT) is common in real-world software development. We propose a sound and efficient technique for NT checking that is also effective on realworld software. Our experiments on wide ranging software benchmarks show that the technique outperforms state-of-the-art NT checkers.
  arXiv  Detail & Related papers  (2024-09-04T22:47:46Z)
• Approximate quantum error correcting codes from conformal field theory [0.0]
  We consider generic 1+1D CFT codes under extensive local dephasing channels. We show that a CFT code with continuous symmetry saturates a bound on the recovery fidelity for covariant codes.
  arXiv  Detail & Related papers  (2024-06-13T19:40:36Z)
• 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)
• Belief Propagation Decoding of Quantum LDPC Codes with Guided Decimation [55.8930142490617]
  We propose a decoder for QLDPC codes based on BP guided decimation (BPGD) BPGD significantly reduces the BP failure rate due to non-convergence.
  arXiv  Detail & Related papers  (2023-12-18T05:58:07Z)
• Tokenization and the Noiseless Channel [71.25796813073399]
  Good tokenizers lead to emphefficient channel usage, where the channel is the means by which some input is conveyed to the model. In machine translation, we find that across multiple tokenizers, the R'enyi entropy with $alpha = 2.5$ has a very strong correlation with textscBleu: $0.78$ in comparison to just $-0.32$ for compressed length.
  arXiv  Detail & Related papers  (2023-06-29T10:32:09Z)
• Compacting Binary Neural Networks by Sparse Kernel Selection [58.84313343190488]
  This paper is motivated by a previously revealed phenomenon that the binary kernels in successful BNNs are nearly power-law distributed. We develop the Permutation Straight-Through Estimator (PSTE) that is able to not only optimize the selection process end-to-end but also maintain the non-repetitive occupancy of selected codewords. Experiments verify that our method reduces both the model size and bit-wise computational costs, and achieves accuracy improvements compared with state-of-the-art BNNs under comparable budgets.
  arXiv  Detail & Related papers  (2023-03-25T13:53:02Z)
• Graph Neural Networks for Channel Decoding [71.15576353630667]
  We showcase competitive decoding performance for various coding schemes, such as low-density parity-check (LDPC) and BCH codes. The idea is to let a neural network (NN) learn a generalized message passing algorithm over a given graph. We benchmark our proposed decoder against state-of-the-art in conventional channel decoding as well as against recent deep learning-based results.
  arXiv  Detail & Related papers  (2022-07-29T15:29:18Z)
• Understanding Deep Learning via Decision Boundary [81.49114762506287]
  We show that the neural network with lower decision boundary (DB) variability has better generalizability. Two new notions, algorithm DB variability and $(epsilon, eta)$-data DB variability, are proposed to measure the decision boundary variability.
  arXiv  Detail & Related papers  (2022-06-03T11:34:12Z)
• 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)
• SAT Encodings for Pseudo-Boolean Constraints Together With At-Most-One Constraints [5.62245362437303]
  We study encodings of Pseudo-Boolean (PB) constraints, a common type of arithmetic constraint. PB(AMO) encodings allow many more instances to be solved within a time limit, and solving time is improved by more than one order of magnitude in some cases.
  arXiv  Detail & Related papers  (2021-10-15T12:53:01Z)
• Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition [161.09660864941603]
  We improve the scalability of Branch and Bound (BaB) algorithms for formally proving input-output properties of neural networks. We present a novel activation-based branching strategy and a BaB framework, named Branch and Dual Network Bound (BaDNB) BaDNB outperforms previous complete verification systems by a large margin, cutting average verification times by factors up to 50 on adversarial properties.
  arXiv  Detail & Related papers  (2021-04-14T09:22:42Z)

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.