An Exact Solver for Satisfiability Modulo Counting with Probabilistic Circuits

• URL: http://arxiv.org/abs/2503.01009v1
• Date: Sun, 02 Mar 2025 20:28:20 GMT
• Title: An Exact Solver for Satisfiability Modulo Counting with Probabilistic Circuits
• Authors: Jinzhao Li, Nan Jiang, Yexiang Xue,
• Abstract summary: An Satisfiability Modulo Counting (SMC) formula is a recently proposed general language to reason.<n>We propose KOCO-SMC, an integrated exact SMC solver that efficiently tracks lower and upper bounds in the probabilistic inference process.
• Score: 16.645967034009225
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Satisfiability Modulo Counting (SMC) is a recently proposed general language to reason about problems integrating statistical and symbolic artificial intelligence. An SMC formula is an extended SAT formula in which the truth values of a few Boolean variables are determined by probabilistic inference. Existing approximate solvers optimize surrogate objectives, which lack formal guarantees. Current exact solvers directly integrate SAT solvers and probabilistic inference solvers resulting in slow performance because of many back-and-forth invocations of both solvers. We propose KOCO-SMC, an integrated exact SMC solver that efficiently tracks lower and upper bounds in the probabilistic inference process. It enhances computational efficiency by enabling early estimation of probabilistic inference using only partial variable assignments, whereas existing methods require full variable assignments. In the experiment, we compare KOCO-SMC with currently available approximate and exact SMC solvers on large-scale datasets and real-world applications. Our approach delivers high-quality solutions with high efficiency.

Related papers

• On Discriminative Probabilistic Modeling for Self-Supervised Representation Learning [85.75164588939185]
  We study the discriminative probabilistic modeling on a continuous domain for the data prediction task of (multimodal) self-supervised representation learning.<n>We conduct generalization error analysis to reveal the limitation of current InfoNCE-based contrastive loss for self-supervised representation learning.<n>We propose a novel non-parametric method for approximating the sum of conditional probability densities required by MIS.
  arXiv  Detail & Related papers  (2024-10-11T18:02:46Z)
• LLaMA-Berry: Pairwise Optimization for O1-like Olympiad-Level Mathematical Reasoning [56.273799410256075]
  The framework combines Monte Carlo Tree Search (MCTS) with iterative Self-Refine to optimize the reasoning path. The framework has been tested on general and advanced benchmarks, showing superior performance in terms of search efficiency and problem-solving capability.
  arXiv  Detail & Related papers  (2024-10-03T18:12:29Z)
• Online POMDP Planning with Anytime Deterministic Guarantees [11.157761902108692]
  Planning under uncertainty can be mathematically formalized using partially observable Markov decision processes (POMDPs) Finding an optimal plan for POMDPs can be computationally expensive and is feasible only for small tasks. We derive a deterministic relationship between a simplified solution that is easier to obtain and the theoretically optimal one.
  arXiv  Detail & Related papers  (2023-10-03T04:40:38Z)
• Solving Satisfiability Modulo Counting for Symbolic and Statistical AI Integration With Provable Guarantees [18.7083987727973]
  Satisfiability Modulo Counting (SMC) encompasses problems that require both symbolic decision-making and statistical reasoning. XOR-SMC transforms the highly intractable SMC into satisfiability problems, by replacing the model counting in SMC with SAT formulae. XOR-SMC finds solutions close to the true optimum, outperforming several baselines which struggle to find good approximations for the intractable model counting in SMC.
  arXiv  Detail & Related papers  (2023-09-16T05:34:59Z)
• Bayesian Quantum State Tomography with Python's PyMC [0.0]
  We show how to use Python-3's open source PyMC probabilistic programming package to transform an otherwise complicated QST optimization problem into a simple form. We show how to use Python-3's open source PyMC probabilistic programming package to transform an otherwise complicated QST optimization problem into a simple form.
  arXiv  Detail & Related papers  (2022-12-20T21:16:28Z)
• Estimating the hardness of SAT encodings for Logical Equivalence Checking of Boolean circuits [58.83758257568434]
  We show that the hardness of SAT encodings for LEC instances can be estimated textitw.r.t some SAT partitioning. The paper proposes several methods for constructing partitionings, which, when used in practice, allow one to estimate the hardness of SAT encodings for LEC with good accuracy.
  arXiv  Detail & Related papers  (2022-10-04T09:19:13Z)
• ML Supported Predictions for SAT Solvers Performance [0.0]
  Internal solver runtime parameters have been collected and analyzed. A machine learning model has been created for the binary classification of the solver's termination behavior.
  arXiv  Detail & Related papers  (2021-12-17T11:17:29Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNF-based SAT and MaxSAT solvers are central to logic synthesis and verification systems. In this work, we propose a one-shot model derived from the Transformer architecture to solve the MaxSAT problem.
  arXiv  Detail & Related papers  (2021-07-15T04:47:35Z)
• Stable Implementation of Probabilistic ODE Solvers [27.70274403550477]
  Probabilistic solvers for ordinary differential equations (ODEs) provide efficient quantification of numerical uncertainty. They suffer from numerical instability when run at high order or with small step-sizes. The present work proposes and examines a solution to this problem. It involves three components: accurate initialisation, a coordinate change preconditioner that makes numerical stability concerns step-size-independent, and square-root implementation.
  arXiv  Detail & Related papers  (2020-12-18T08:35:36Z)
• Efficient semidefinite-programming-based inference for binary and multi-class MRFs [83.09715052229782]
  We propose an efficient method for computing the partition function or MAP estimate in a pairwise MRF. We extend semidefinite relaxations from the typical binary MRF to the full multi-class setting, and develop a compact semidefinite relaxation that can again be solved efficiently using the solver.
  arXiv  Detail & Related papers  (2020-12-04T15:36:29Z)
• Adaptive Sampling for Best Policy Identification in Markov Decision Processes [79.4957965474334]
  We investigate the problem of best-policy identification in discounted Markov Decision (MDPs) when the learner has access to a generative model. The advantages of state-of-the-art algorithms are discussed and illustrated.
  arXiv  Detail & Related papers  (2020-09-28T15:22:24Z)

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.