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

• A Comparative Study on Reasoning Patterns of OpenAI's o1 Model [69.08287909042421]
  We show that OpenAI's o1 model has achieved the best performance on most datasets. We also provide a detailed analysis on several reasoning benchmarks.
  arXiv  Detail & Related papers  (2024-10-17T15:09:03Z)
• 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)
• Lifted Algorithms for Symmetric Weighted First-Order Model Sampling [7.007419073974192]
  We prove the domain-liftability under sampling for the two-variables fragment of first-order logic with counting quantifiers. We then show that this result continues to hold even in the presence of cardinality constraints. Our algorithm outperforms a start-of-the-art WMS sampler by a substantial margin.
  arXiv  Detail & Related papers  (2023-08-17T07:40:47Z)
• Efficient Model-Free Exploration in Low-Rank MDPs [76.87340323826945]
  Low-Rank Markov Decision Processes offer a simple, yet expressive framework for RL with function approximation. Existing algorithms are either (1) computationally intractable, or (2) reliant upon restrictive statistical assumptions. We propose the first provably sample-efficient algorithm for exploration in Low-Rank MDPs.
  arXiv  Detail & Related papers  (2023-07-08T15:41:48Z)
• 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.