2026-07-23T08:35:16Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:15299 2024-03-06T10:55:04Z ddc:004 open_access

Integrating Tree Decompositions into Decision Heuristics of Propositional Model Counters (Short Paper) Korhonen, Tuukka Järvisalo, Matti propositional model counting decision heuristics tree decompositions empirical evaluation 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Tuukka Korhonen and Matti Järvisalo 2021 Is Part Of LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CP.2021.8 urn:nbn:de:0030-drops-152992 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.8 eng https://creativecommons.org/licenses/by/4.0/legalcode