Towards Projected and Incremental Pseudo-Boolean Model Counting

TL;DR

This paper introduces PBCount2, the first exact Pseudo-Boolean model counter supporting projected and incremental counting, significantly improving benchmark performance over existing methods.

Contribution

The paper presents PBCount2, a novel exact PB model counter with support for projected and incremental counting, filling key gaps in existing tools.

Findings

PBCount2 completed 1.40x more benchmarks for projected counting.

PBCount2 completed 1.18x more benchmarks for incremental counting.

Supports both projected and incremental model counting in PB formulas.

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.