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.
翻译:本文介绍SharpSAT-TD系统,该系统作为我们在2021-2023年模型计数竞赛中未加权赛道和加权赛道的参赛工具,共获得竞赛不同赛道的6个第一名。SharpSAT-TD基于SharpSAT [Thurley, SAT 2006]构建,其主要创新改进在于采用了作者在[CP 2021]中提出的基于树分解的变量选择启发式策略。与[CP 2021]中评估的SharpSAT-TD版本不同,当前版本(可从https://github.com/Laakeri/sharpsat-td获取)相比原始SharpSAT还包含了其他重要改进,例如新增了预处理模块。