License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CP.2021.8
URN: urn:nbn:de:0030-drops-152992
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/15299/
Korhonen, Tuukka ;
Järvisalo, Matti
Integrating Tree Decompositions into Decision Heuristics of Propositional Model Counters (Short Paper)
Abstract
Propositional model counting (#SAT), the problem of determining the number of satisfying assignments of a propositional formula, is the archetypical #P-complete problem with a wide range of applications in AI. In this paper, we show that integrating tree decompositions of low width into the decision heuristics of a reference exact model counter (SharpSAT) significantly improves its runtime performance. In particular, our modifications to SharpSAT (and its derivant GANAK) lift the runtime efficiency of SharpSAT to the extent that it outperforms state-of-the-art exact model counters, including earlier-developed model counters that exploit tree decompositions.
BibTeX - Entry
@InProceedings{korhonen_et_al:LIPIcs.CP.2021.8,
author = {Korhonen, Tuukka and J\"{a}rvisalo, Matti},
title = {{Integrating Tree Decompositions into Decision Heuristics of Propositional Model Counters}},
booktitle = {27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
pages = {8:1--8:11},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-211-2},
ISSN = {1868-8969},
year = {2021},
volume = {210},
editor = {Michel, Laurent D.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/15299},
URN = {urn:nbn:de:0030-drops-152992},
doi = {10.4230/LIPIcs.CP.2021.8},
annote = {Keywords: propositional model counting, decision heuristics, tree decompositions, empirical evaluation}
}
