@COMMENT This file was generated by bib2html.pl version 0.94
@COMMENT written by Patrick Riley
@COMMENT This file came from Kuldeep S. Meel's publication pages at
@COMMENT http://www.comp.nus.edu.sg/~meel/publications/
@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.
},
}