First Place in Model Counting Competition 2021

The SharpSAT-TD exact propositional model counter, implemented by Tuukka Korhonen of the Constraint Reasoning and Optimization group, ranks first in Model Counting Competition 2021, the annual international competitive event for state-of-the-art model counting systems.

The SharpSAT-TD model counter by Tuukka Korhonen and Matti Järvisalo of the Constraint Reasoning and Optimization group has won both the unweighted and weighted exact model counting tracks of Model Counting Competition 2021 (MCC 2021). MCC is the main international competitive event for state-of-the-art model counting systems. A key component of SharpSAT-TD is a novel approach to employing information on a tree decomposition of the propositional formula at hand for guiding the search process of the model counter.