PBCounter: Weighted Model Counting on Pseudo-Boolean Formulas

• URL: http://arxiv.org/abs/2312.15877v1
• Date: Tue, 26 Dec 2023 04:03:23 GMT
• Title: PBCounter: Weighted Model Counting on Pseudo-Boolean Formulas
• Authors: Yong Lai, Zhenghang Xu, Minghao Yin
• Abstract summary: 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.
• Score: 18.02313966511695
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: In Weighted Model Counting (WMC), we assign weights to literals and compute the sum of the weights of the models of a given propositional formula where the weight of an assignment is the product of the weights of its literals. The current WMC solvers work on Conjunctive Normal Form (CNF) formulas. However, CNF is not a natural representation for human-being in many applications. Motivated by the stronger expressive power of pseudo-Boolean (PB) formulas than CNF, we propose to perform WMC on PB formulas. Based on a recent dynamic programming algorithm framework called ADDMC for WMC, 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, where the latter tools work on CNF with encoding methods that convert PB constraints into a CNF formula. The experiments on three domains of benchmarks show that PBCounter is superior to the model counters on CNF formulas.

Related papers

• Engineering an Exact Pseudo-Boolean Model Counter [38.901687092266094]
  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.
  arXiv  Detail & Related papers  (2023-12-19T17:14:06Z)
• 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)
• Benchmarking Diverse-Modal Entity Linking with Generative Models [78.93737257356784]
  We construct a benchmark for diverse-modal EL (DMEL) from existing EL datasets. To approach the DMEL task, we proposed a generative diverse-modal model (GDMM) following a multimodal-encoder-decoder paradigm. GDMM builds a stronger DMEL baseline, outperforming state-of-the-art task-specific EL models by 8.51 F1 score on average.
  arXiv  Detail & Related papers  (2023-05-27T02:38:46Z)
• 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)
• Low-variance estimation in the Plackett-Luce model via quasi-Monte Carlo sampling [58.14878401145309]
  We develop a novel approach to producing more sample-efficient estimators of expectations in the PL model. We illustrate our findings both theoretically and empirically using real-world recommendation data from Amazon Music and the Yahoo learning-to-rank challenge.
  arXiv  Detail & Related papers  (2022-05-12T11:15:47Z)
• Rule-based Shielding for Partially Observable Monte-Carlo Planning [78.05638156687343]
  We propose two contributions to Partially Observable Monte-Carlo Planning (POMCP) The first is a method for identifying unexpected actions selected by POMCP with respect to expert prior knowledge of the task. The second is a shielding approach that prevents POMCP from selecting unexpected actions. We evaluate our approach on Tiger, a standard benchmark for POMDPs, and a real-world problem related to velocity regulation in mobile robot navigation.
  arXiv  Detail & Related papers  (2021-04-28T14:23:38Z)
• On Batch Normalisation for Approximate Bayesian Inference [102.94525205971873]
  We show that batch-normalisation does not affect the optimum of the evidence lower bound (ELBO) We also study the Monte Carlo Batch Normalisation (MCBN) algorithm, proposed as an approximate inference technique parallel to MC Dropout.
  arXiv  Detail & Related papers  (2020-12-24T12:40:11Z)
• DPMC: Weighted Model Counting by Dynamic Programming on Project-Join Trees [26.25724674611307]
  We propose a unifying dynamic-programming framework to compute exact literal-weighted model counts of formulas in conjunctive normal form. At the center of our framework are project-join trees, which specify efficient project-join orders. We show that our dynamic-programming model-counting framework DPMC is competitive with the state-of-the-art exact weighted model counters cachet, c2d, d4, and miniC2D.
  arXiv  Detail & Related papers  (2020-08-20T03:09:09Z)
• MCMC Should Mix: Learning Energy-Based Model with Neural Transport Latent Space MCMC [110.02001052791353]
  Learning energy-based model (EBM) requires MCMC sampling of the learned model as an inner loop of the learning algorithm. We show that the model has a particularly simple form in the space of the latent variables of the backbone model.
  arXiv  Detail & Related papers  (2020-06-12T01:25:51Z)
• 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)

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.