Efficient Incremental #SAT via Cross-Instance Knowledge Reuse
For users of probabilistic reasoning tools, this work offers a practical speedup in incremental model counting tasks, though the gains are domain-specific and incremental.
The paper tackles incremental model counting for sequences of structurally similar formulas, proposing a persistent caching mechanism that reuses component data across solver calls. Experiments show improved performance over current model counters in argumentation and soft core problems.
Model counting ($\#\text{SAT}$) is a fundamental yet $\#\text{P}$-complete problem central to probabilistic reasoning. In this work, we address \textit{incremental model counting}, where sequences of structurally similar formulas must be counted. We propose an approach that amortizes computation via a persistent caching mechanism, retaining component data across solver calls to avoid redundant search. Additionally, we investigate branching heuristics adapted for this setting. We focus on the problems of argumentation and soft core, for which incremental model counting is natural. Experiments demonstrate that our method improves performance compared to current model counters, highlighting the capability of structure-aware reuse in dynamic environments.