SharpSAT-TD in Model Counting Competitions 2021-2023

TL;DR

SharpSAT-TD is a competitive model counting solver that integrates tree decomposition-based heuristics and new preprocessing techniques, achieving multiple first-place wins in recent competitions.

Contribution

The paper introduces SharpSAT-TD, a novel model counter that combines tree decomposition heuristics with enhanced preprocessing, outperforming previous versions and competitors.

Findings

Won 6 first places in recent competitions

Incorporates tree decomposition in variable selection

Features significant modifications over original SharpSAT

Abstract

We describe SharpSAT-TD, our submission to the unweighted and weighted tracks of the Model Counting Competition in 2021-2023, which has won in total $6$ first places in different tracks of the competition. SharpSAT-TD is based on SharpSAT [Thurley, SAT 2006], with the primary novel modification being the use of tree decompositions in the variable selection heuristic as introduced by the authors in [CP 2021]. Unlike the version of SharpSAT-TD evaluated in [CP 2021], the current version that is available in https://github.com/Laakeri/sharpsat-td features also other significant modifications compared to the original SharpSAT, for example, a new preprocessor.