Integrating Tree Decompositions into Decision Heuristics of Propositional Model Counters (Short Paper)
Korhonen, Tuukka, Järvisalo, Matti
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.
Topics & Concepts
Counting problemCompetition (biology)SPARK (programming language)Computer scienceProbabilistic logicVariety (cybernetics)Counting processTheoretical computer scienceArtificial intelligenceMathematicsAlgorithmStatisticsProgramming languageEcologyBiologyBayesian Modeling and Causal InferenceData Management and AlgorithmsGraph Theory and Algorithms