# The Model Counting Competition 2020

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

## Key facts

- Cited by 24 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 2 Dec 2020.

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

- [NeuroBack: Improving CDCL SAT Solving using Graph Neural Networks](https://mlsanity.com/paper/2110.14053/) (2021)
- [Rushing and Strolling among Answer Sets -- Navigation Made Easy](https://mlsanity.com/paper/2112.07596/) (2021)
- [On the Hardness of Probabilistic Neurosymbolic Learning](https://mlsanity.com/paper/2406.04472/) (2024)
- [Partition Function Estimation: A Quantitative Study](https://mlsanity.com/paper/2105.11132/) (2021)
- [Treewidth-aware Reductions of Normal ASP to SAT -- Is Normal ASP Harder than SAT after All?](https://mlsanity.com/paper/2210.03553/) (2022)
- [Rounding Meets Approximate Model Counting](https://mlsanity.com/paper/2305.09247/) (2023)
- [Utilizing Treewidth for Quantitative Reasoning on Epistemic Logic Programs](https://mlsanity.com/paper/2108.03022/) (2021)
- [DPMS: An ADD-Based Symbolic Approach for Generalized MaxSAT Solving](https://mlsanity.com/paper/2205.03747/) (2022)
- [Projected Model Counting: Beyond Independent Support](https://mlsanity.com/paper/2110.09171/) (2021)
- [A Quantitative Symbolic Approach to Individual Human Reasoning](https://mlsanity.com/paper/2205.05030/) (2022)
- [IASCAR: Incremental Answer Set Counting by Anytime Refinement](https://mlsanity.com/paper/2311.07233/) (2023)
- [Model Counting in the Wild](https://mlsanity.com/paper/2408.07059/) (2024)
- [Counting and Reasoning with Plans](https://mlsanity.com/paper/2502.00145/) (2025)
- [Advanced Tools and Methods for Treewidth-Based Problem Solving -- Extended Abstract](https://mlsanity.com/paper/2208.11340/) (2022)
- [Solving Projected Model Counting by Utilizing Treewidth and its Limits](https://mlsanity.com/paper/2305.19212/) (2023)
- [Quantum Algorithms for Weighted Constrained Sampling and Weighted Model Counting](https://mlsanity.com/paper/2407.12816/) (2024)
- [The Gradient of Algebraic Model Counting](https://mlsanity.com/paper/2502.18406/) (2025)
- [Generation and Prediction of Difficult Model Counting Instances](https://mlsanity.com/paper/2212.02893/) (2022)
- [Extended Version of: On the Structural Hardness of Answer Set Programming: Can Structure Efficiently Confine the Power of Disjunctions?](https://mlsanity.com/paper/2402.03539/) (2024)
- [Techniques for Measuring the Inferential Strength of Forgetting Policies](https://mlsanity.com/paper/2404.02454/) (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)
- [Numerical Considerations in Weighted Model Counting](https://mlsanity.com/paper/2508.06264/) (2025)
- [CSB: A Counting and Sampling tool for Bit-vectors](https://mlsanity.com/paper/2607.04142/) (2026)

## Abstract (arXiv)

Many computational problems in modern society account to probabilistic reasoning, statistics, and combinatorics. A variety of these real-world questions can be solved by representing the question in (Boolean) formulas and associating the number of models of the formula directly with the answer to the question. Since there has been an increasing interest in practical problem solving for model counting over the last years, the Model Counting (MC) Competition was conceived in fall 2019. The competition aims to foster applications, identify new challenging benchmarks, and to promote new solvers and improve established solvers for the model counting problem and versions thereof. We hope that the results can be a good indicator of the current feasibility of model counting and spark many new applications. In this paper, we report on details of the Model Counting Competition 2020, about carrying out the competition, and the results. The competition encompassed three versions of the model counting problem, which we evaluated in separate tracks. The first track featured the model counting problem (MC), which asks for the number of models of a given Boolean formula. On the second track, we challenged developers to submit programs that solve the weighted model counting problem (WMC). The last track was dedicated to projected model counting (PMC). In total, we received a surprising number of 9 solvers in 34 versions from 8 groups.