• Classified by Research Topic • Sorted by Date • Classified by Publication Type •
Engineering an Efficient Probabilistic Exact Model Counter.
Mate Soos, and Kuldeep S. Meel.
In Proceedings of International Conference on Computer-Aided Verification (CAV), pp. 72–91, 2025.
Given a formula F , the problem of model counting, also known as #SAT, is to compute the number of satisfying assignments of F . While model counting has emerged as a crucial primitive in diverse domains from quantitative information flow analysis to neural network verification, scalability remains a fundamental challenge despite advances in both exact and approximate counting techniques. We present $$\textsfGanak2$$ Ganak 2 , a novel framework that achieves substantial performance improvements through three key technical innovations: (1) refined residual formula processing incorporating SAT-specific techniques while maintaining seamless state transitions, (2) dual independent set framework maintaining distinct SAT-eligibility and decision sets, and (3) chronological backtracking specifically adapted to model counting. Our empirical evaluation on 1600 previous model counting competition instances demonstrates that $$\textsfGanak2$$ Ganak 2 successfully computes counts for 1121 instances within the one hour time limit, compared to 1032 instances by the prior state of the art approach, representing an 8.7% improvement. This progress is especially remarkable considering the extensive development and refinement of model counting tools over the years, driven by yearly competitive evaluation in the field.
@inproceedings{SM25a,
title={Engineering an Efficient Probabilistic Exact Model Counter},
author={Soos, Mate and Meel, Kuldeep S.},
booktitle=CAV,
pages={72--91},
year={2025},
bib2html_rescat={Counting, Solver Engineering},
bib2html_pubtype={Refereed Conference},
bib2html_dl_pdf=
{https://link.springer.com/chapter/10.1007/978-3-031-98682-6_5},
abstract={
Given a formula F , the problem of model counting, also known as #SAT, is to
compute the number of satisfying assignments of F . While model counting has
emerged as a crucial primitive in diverse domains from quantitative
information flow analysis to neural network verification, scalability
remains a fundamental challenge despite advances in both exact and
approximate counting techniques. We present $$\textsf{Ganak2}$$ Ganak 2 , a
novel framework that achieves substantial performance improvements through
three key technical innovations: (1) refined residual formula processing
incorporating SAT-specific techniques while maintaining seamless state
transitions, (2) dual independent set framework maintaining distinct
SAT-eligibility and decision sets, and (3) chronological backtracking
specifically adapted to model counting. Our empirical evaluation on 1600
previous model counting competition instances demonstrates that
$$\textsf{Ganak2}$$ Ganak 2 successfully computes counts for 1121 instances
within the one hour time limit, compared to 1032 instances by the prior
state of the art approach, representing an 8.7% improvement. This progress
is especially remarkable considering the extensive development and
refinement of model counting tools over the years, driven by yearly
competitive evaluation in the field.
},
}
Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Thu Sep 10, 2026 16:32:38