Engineering an Exact Pseudo-Boolean Model Counter
- URL: http://arxiv.org/abs/2312.12341v2
- Date: Sun, 18 Feb 2024 01:49:00 GMT
- Title: Engineering an Exact Pseudo-Boolean Model Counter
- Authors: Suwei Yang and Kuldeep S. Meel
- Abstract summary: We propose the first exact Pseudo-Boolean model counter, PBCount, that relies on knowledge compilation approach via algebraic decision diagrams.
Our empirical evaluation shows that PBCount can compute counts for 1513 instances while the current state-of-the-art approach could only handle 1013 instances.
- Score: 38.901687092266094
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Model counting, a fundamental task in computer science, involves determining
the number of satisfying assignments to a Boolean formula, typically
represented in conjunctive normal form (CNF). While model counting for CNF
formulas has received extensive attention with a broad range of applications,
the study of model counting for Pseudo-Boolean (PB) formulas has been
relatively overlooked. Pseudo-Boolean formulas, being more succinct than
propositional Boolean formulas, offer greater flexibility in representing
real-world problems. Consequently, there is a crucial need to investigate
efficient techniques for model counting for PB formulas.
In this work, we propose the first exact Pseudo-Boolean model counter,
PBCount, that relies on knowledge compilation approach via algebraic decision
diagrams. Our extensive empirical evaluation shows that PBCount can compute
counts for 1513 instances while the current state-of-the-art approach could
only handle 1013 instances. Our work opens up several avenues for future work
in the context of model counting for PB formulas, such as the development of
preprocessing techniques and exploration of approaches other than knowledge
compilation.
Related papers
- Exploring the Limit of Outcome Reward for Learning Mathematical Reasoning [65.2421542320293]
Reasoning abilities are crucial components of general intelligence.
Recent advances by proprietary companies, such as o-series models of OpenAI, have made remarkable progress on reasoning tasks.
This paper proposes a new RL framework, termed OREAL, to pursue the performance limit that can be achieved through textbfOutcome textbfREwtextbfArd-based reinforcement textbfLearning for mathematical reasoning tasks.
arXiv Detail & Related papers (2025-02-10T18:57:29Z) - BRiTE: Bootstrapping Reinforced Thinking Process to Enhance Language Model Reasoning [78.63421517563056]
Large Language Models (LLMs) have demonstrated remarkable capabilities in complex reasoning tasks.
We present a unified probabilistic framework that formalizes LLM reasoning through a novel graphical model.
We introduce the Bootstrapping Reinforced Thinking Process (BRiTE) algorithm, which works in two steps.
arXiv Detail & Related papers (2025-01-31T02:39:07Z) - Towards Projected and Incremental Pseudo-Boolean Model Counting [32.92936885170422]
We introduce the first exact Pseudo-Boolean (PB) model counter with support for projected and incremental model counting.
In our evaluations, PBCount2 completed at least 1.40x the number of benchmarks of competing methods for projected model counting and at least 1.18x of competing methods in incremental model counting.
arXiv Detail & Related papers (2024-12-19T03:11:33Z) - PBCounter: Weighted Model Counting on Pseudo-Boolean Formulas [18.02313966511695]
We implement a weighted PB counting tool PBCounter.
We compare PBCounter with the state-of-the-art weighted model counters SharpSAT-TD, ExactMC, D4, and ADDMC.
The experiments on three domains of benchmarks show that PBCounter is superior to the model counters on CNF formulas.
arXiv Detail & Related papers (2023-12-26T04:03:23Z) - Fast Converging Anytime Model Counting [34.295512073482186]
This paper designs a new anytime approach called PartialKC for approximate model counting.
Our empirical analysis demonstrates that PartialKC achieves significant scalability and accuracy over prior state-of-the-art approximate counters.
Interestingly, the empirical results show that PartialKC reaches convergence for many instances and therefore provides exact model counting performance comparable to state-of-the-art exact counters.
arXiv Detail & Related papers (2022-12-19T12:01:28Z) - Low-Rank Constraints for Fast Inference in Structured Models [110.38427965904266]
This work demonstrates a simple approach to reduce the computational and memory complexity of a large class of structured models.
Experiments with neural parameterized structured models for language modeling, polyphonic music modeling, unsupervised grammar induction, and video modeling show that our approach matches the accuracy of standard models at large state spaces.
arXiv Detail & Related papers (2022-01-08T00:47:50Z) - How to Design Sample and Computationally Efficient VQA Models [53.65668097847456]
We find that representing the text as probabilistic programs and images as object-level scene graphs best satisfy these desiderata.
We extend existing models to leverage these soft programs and scene graphs to train on question answer pairs in an end-to-end manner.
arXiv Detail & Related papers (2021-03-22T01:48:16Z) - Control as Hybrid Inference [62.997667081978825]
We present an implementation of CHI which naturally mediates the balance between iterative and amortised inference.
We verify the scalability of our algorithm on a continuous control benchmark, demonstrating that it outperforms strong model-free and model-based baselines.
arXiv Detail & Related papers (2020-07-11T19:44:09Z) - On the Approximability of Weighted Model Integration on DNF Structures [13.986963122264632]
We show that weighted model integration on DNF structures can indeed be approximated for a class of weight functions.
Our approximation algorithm is based on three subroutines, each which can be a weak (i.e., approximate), or a strong (i.e., exact) oracle.
arXiv Detail & Related papers (2020-02-17T00:29:41Z) - Approximate Weighted First-Order Model Counting: Exploiting Fast
Approximate Model Counters and Symmetry [16.574508244279098]
We present ApproxWFOMC, a novel anytime method for efficiently bounding the weighted first-order model count.
The algorithm has applications to inference in a variety of first-order probabilistic representations.
We show how our algorithm outperforms existing approximate and exact techniques for inference in first-order probabilistic models.
arXiv Detail & Related papers (2020-01-15T12:21:06Z)
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.