• 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 Sun Apr 14, 2024 11:15:51