Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2605.00671 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911638718775296 |
|---|---|
| author | Bartal, Uriya Fried, Dror Lagniez, Jean-Marie |
| author_facet | Bartal, Uriya Fried, Dror Lagniez, Jean-Marie |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_00671 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Efficient Incremental #SAT via Cross-Instance Knowledge Reuse Bartal, Uriya Fried, Dror Lagniez, Jean-Marie Logic in Computer Science 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. |
| title | Efficient Incremental #SAT via Cross-Instance Knowledge Reuse |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2605.00671 |