Engineering an Exact Pseudo-Boolean Model Counter
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.
Code (1)
Tasks
modelSimilar Papers 제목 키워드 기반
PBCounter: Weighted Model Counting on Pseudo-Boolean Formulas
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 lit…
modelTowards Projected and Incremental Pseudo-Boolean Model Counting
Model counting is a fundamental task that involves determining the number of satisfying assignments to a logical formula, typically in conjunctive normal form (CNF). While CNF model counting has received extensive attent…
DPO: Dynamic-Programming Optimization on Hybrid Constraints
In Bayesian inference, the most probable explanation (MPE) problem requests a variable instantiation with the highest probability given some evidence. Since a Bayesian network can be encoded as a literal-weighted CNF for…
Bayesian InferenceQuadratization of Symmetric Pseudo-Boolean Functions
A pseudo-Boolean function is a real-valued function $f(x)=f(x_1,x_2,\ldots,x_n)$ of $n$ binary variables; that is, a mapping from $\{0,1\}^n$ to $\mathbb{R}$. For a pseudo-Boolean function $f(x)$ on $\{0,1\}^n$, we say t…
A Pseudo-Boolean Polynomials Approach for Image Edge Detection
We introduce a novel approach for image edge detection based on pseudo-Boolean polynomials for image patches. We show that patches covering edge regions in the image result in pseudo-Boolean polynomials with higher degre…
Edge Detection