Efficient Incremental #SAT via Cross-Instance Knowledge Reuse

TL;DR

This paper introduces a new incremental model counting method that leverages persistent caching and specialized heuristics to efficiently reuse knowledge across similar problem instances, improving performance.

Contribution

The work presents a novel approach combining persistent caching and adapted heuristics for incremental model counting, specifically targeting argumentation and soft core problems.

Findings

Method outperforms existing model counters on targeted problems.

Persistent caching significantly reduces redundant computation.

Structure-aware reuse enhances efficiency in dynamic environments.

Abstract

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.