# SharpSAT-TD in Model Counting Competitions 2021-2023

arXiv: https://arxiv.org/abs/2308.15819 · HTML: https://mlsanity.com/paper/2308.15819/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 2 of its 10 references that are in the map.
- First posted on arXiv 30 Aug 2023.

## Builds on (most cited first, 2 of 2)

- [Computing Tree Decompositions with FlowCutter: PACE 2017 Submission](https://mlsanity.com/paper/1709.08949/) (2017)
- [Graph Bisection with Pareto-Optimization](https://mlsanity.com/paper/1504.03812/) (2015)

## Built on by (most cited first, 3 of 3)

- [Pruning Boolean d-DNNF Circuits Through Tseitin-Awareness](https://mlsanity.com/paper/2407.17951/) (2024)
- [Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits](https://mlsanity.com/paper/2503.01009/) (2025)
- [Pseudo-Boolean d-DNNF Compilation for Expressive Feature Modeling Constructs](https://mlsanity.com/paper/2505.05976/) (2025)

## Abstract (arXiv)

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.