• Classified by Research Topic • Sorted by Date • Classified by Publication Type •
Symmetric Component Caching for Model Counting on Combinatorial Instances .
Timothy van Bremen, Vincent Derkinderen, Shubham Sharma, Subhajit Roy and Kuldeep S. Meel .
In Proceedings of AAAI Conference on Artificial Intelligence (AAAI), February 2021.
Given a propositional formula $\psi$, the model counting problem, also referred to as #SAT, seeks to compute the number of satisfying assignments (or models) of $\psi$. Modern search-based model counting algorithms are built on conflict-driven clause learning, combined with the caching of certain subformulas (called components) encountered during the search process. Despite significant progress in these algorithms over the years, state-of-the-art model counters often struggle to handle large but structured instances that typically arise in combinatorial settings. Motivated by the observation that these counters do not exploit the inherent symmetries exhibited in such instances, we revisit the component caching architecture employed in current counters and introduce a novel caching scheme that focuses on identifying symmetric components. We first prove the soundness of our approach, and then integrate it into the state-of-the-art model counter GANAK. Our extensive experiments on hard combinatorial instances demonstrate that the resulting counter, SymGANAK, leads to improvements over GANAK both in terms of PAR-2 score and the number of instances solved.
@inproceedings{BDSRM21,
title={
Symmetric Component Caching for Model Counting on Combinatorial Instances
},
author={
Timothy van Bremen and Vincent Derkinderen and Shubham Sharma and Subhajit
Roy and Kuldeep S. Meel
},
booktitle=AAAI,
month=feb,
year={2021},
bib2html_rescat={Counting},
bib2html_pubtype={Refereed Conference},
bib2html_dl_pdf={../Papers/aaai21-bdsrm.pdf},
abstract={
Given a propositional formula $\psi$, the model counting problem, also
referred to as #SAT, seeks to compute the number of satisfying assignments
(or models) of $\psi$. Modern search-based model counting algorithms are
built on conflict-driven clause learning, combined with the caching of
certain subformulas (called components) encountered during the search
process. Despite significant progress in these algorithms over the years,
state-of-the-art model counters often struggle to handle large but
structured instances that typically arise in combinatorial settings.
Motivated by the observation that these counters do not exploit the inherent
symmetries exhibited in such instances, we revisit the component caching
architecture employed in current counters and introduce a novel caching
scheme that focuses on identifying symmetric components. We first prove the
soundness of our approach, and then integrate it into the state-of-the-art
model counter GANAK. Our extensive experiments on hard combinatorial
instances demonstrate that the resulting counter, SymGANAK, leads to
improvements over GANAK both in terms of PAR-2 score and the number of
instances solved.
},
}
Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Tue Apr 28, 2026 01:27:21