• Classified by Research Topic • Sorted by Date • Classified by Publication Type •
Towards Projected and Incremental Pseudo-Boolean Model Counting.
Suwei Yang, and Kuldeep S. Meel.
In Proceedings of AAAI Conference on Artificial Intelligence (AAAI), February 2025.
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 attention over recent decades, interest in Pseudo-Boolean (PB) model counting is just emerging partly due to the greater flexibility of PB formulas. As such, we observed feature gaps in existing PB counters such as a lack of support for projected and incremental settings, which could hinder adoption. In this work, our main contribution is the introduction of the PB model counter PBCount2, the first exact PB model counter with support for projected and incremental model counting. Our counter, PBCount2, uses our Least Occurrence Weighted Min Degree (LOW-MD) computation ordering heuristic to support projected model counting and a cache mechanism to enable 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.
@inproceedings{YM25,
title={Towards Projected and Incremental Pseudo-Boolean Model Counting},
booktitle=AAAI,
author={Yang, Suwei and Meel, Kuldeep S.},
abstract={
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 attention over
recent decades, interest in Pseudo-Boolean (PB) model counting is just
emerging partly due to the greater flexibility of PB formulas. As such, we
observed feature gaps in existing PB counters such as a lack of support for
projected and incremental settings, which could hinder adoption. In this
work, our main contribution is the introduction of the PB model counter
PBCount2, the first exact PB model counter with support for projected and
incremental model counting. Our counter, PBCount2, uses our Least Occurrence
Weighted Min Degree (LOW-MD) computation ordering heuristic to support
projected model counting and a cache mechanism to enable 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.
},
year={2025},
month=feb,
bib2html_rescat={Counting},
bib2html_pubtype={Refereed Conference},
bib2html_dl_pdf={https://arxiv.org/abs/2412.14485},
}
Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Tue Apr 28, 2026 01:27:21