• Classified by Research Topic • Sorted by Date • Classified by Publication Type •
On Top-Down Pseudo-Boolean Model Counting.
Suwei Yang, Yong Lai and Kuldeep S. Meel.
In Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (SAT), pp. 31:1–31:10, August 2025.
Pseudo-Boolean model counting involves computing the number of satisfying assignments of a given pseudo-Boolean (PB) formula. In recent years, PB model counting has seen increased interest partly owing to the succinctness of PB formulas over typical propositional Boolean formulas in conjunctive normal form (CNF) at describing problem constraints. In particular, the research community has developed tools to tackle exact PB model counting. These recently developed counters follow one of the two existing major designs for model counters, namely the bottom-up model counter design. A natural question would be whether the other major design, the top-down model counter paradigm, would be effective at PB model counting, especially when the top-down design offered superior performance in CNF model counting literature. In this work, we investigate the aforementioned top-down design for PB model counting and introduce the first exact top-down PB model counter, PBMC. PBMC is a top-down search-based counter for PB formulas, with a new variable decision heuristic that considers variable coefficients. Through our evaluations, we highlight the superior performance of PBMC at PB model counting compared to the existing state-of-the-art counters PBCount, PBCounter, and Ganak. In particular, PBMC could count for 1849 instances while the next-best competing method, PBCount, could only count for 1773 instances, demonstrating the potential of a top-down PB counter design.
@inproceedings{YLM25,
title={On Top-Down Pseudo-Boolean Model Counting},
author={Yang, Suwei and Lai, Yong and Meel, Kuldeep S.},
booktitle=SAT,
pages={31:1--31:10},
year={2025},
month=aug,
bib2html_rescat={Counting},
bib2html_pubtype={Refereed Conference},
bib2html_dl_pdf=
{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.31},
abstract={
Pseudo-Boolean model counting involves computing the number of satisfying
assignments of a given pseudo-Boolean (PB) formula. In recent years, PB
model counting has seen increased interest partly owing to the succinctness
of PB formulas over typical propositional Boolean formulas in conjunctive
normal form (CNF) at describing problem constraints. In particular, the
research community has developed tools to tackle exact PB model counting.
These recently developed counters follow one of the two existing major
designs for model counters, namely the bottom-up model counter design. A
natural question would be whether the other major design, the top-down model
counter paradigm, would be effective at PB model counting, especially when
the top-down design offered superior performance in CNF model counting
literature. In this work, we investigate the aforementioned top-down design
for PB model counting and introduce the first exact top-down PB model
counter, PBMC. PBMC is a top-down search-based counter for PB formulas, with
a new variable decision heuristic that considers variable coefficients.
Through our evaluations, we highlight the superior performance of PBMC at PB
model counting compared to the existing state-of-the-art counters PBCount,
PBCounter, and Ganak. In particular, PBMC could count for 1849 instances
while the next-best competing method, PBCount, could only count for 1773
instances, demonstrating the potential of a top-down PB counter design.
},
}
Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Tue Apr 28, 2026 01:27:21