Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Model Counting Competitions 2021-2023

Johannes K. Fichte, Markus Hecher

TL;DR

This paper provides a comprehensive review of the MCC over 2021–2023, detailing four counting variants (MC, WMC, PMC, PWMC), their tracks, and the experimental framework. It covers instance collection, benchmarking infrastructure, solver families, and track-specific results, highlighting breakthroughs from SharpSAT-TD, D4, GPMC, and portfolio approaches like Arjun-GANAK-ApproxMC. Beyond results, the work emphasizes reproducibility via public datasets, Zenodo archives, and copperbench tooling, showcasing how the community can build on these benchmarks. The study reveals substantial progress in both exact and approximate counting, underscores the value of preprocessing and decomposition techniques, and outlines future directions including certification, robust benchmarking, and enhanced replication for ongoing advancement in counting under CNF encodings.

Abstract

Modern society is full of computational challenges that rely on probabilistic reasoning, statistics, and combinatorics. Interestingly, many of these questions can be formulated by encoding them into propositional formulas and then asking for its number of models. With a growing interest in practical problem-solving for tasks that involve model counting, the community established the Model Counting (MC) Competition in fall of 2019 with its first iteration in 2020. The competition aims at advancing applications, identifying challenging benchmarks, fostering new solver development, and enhancing existing solvers for model counting problems and their variants. The first iteration, brought together various researchers, identified challenges, and inspired numerous new applications. In this paper, we present a comprehensive overview of the 2021-2023 iterations of the Model Counting Competition. We detail its execution and outcomes. The competition comprised four tracks, each focusing on a different variant of the model counting problem. The first track centered on the model counting problem (MC), which seeks the count of models for a given propositional formula. The second track challenged developers to submit programs capable of solving the weighted model counting problem (WMC). The third track was dedicated to projected model counting (PMC). Finally, we initiated a track that combined projected and weighted model counting (PWMC). The competition continued with a high level of participation, with seven to nine solvers submitted in various different version and based on quite diverging techniques.

The Model Counting Competitions 2021-2023

TL;DR

This paper provides a comprehensive review of the MCC over 2021–2023, detailing four counting variants (MC, WMC, PMC, PWMC), their tracks, and the experimental framework. It covers instance collection, benchmarking infrastructure, solver families, and track-specific results, highlighting breakthroughs from SharpSAT-TD, D4, GPMC, and portfolio approaches like Arjun-GANAK-ApproxMC. Beyond results, the work emphasizes reproducibility via public datasets, Zenodo archives, and copperbench tooling, showcasing how the community can build on these benchmarks. The study reveals substantial progress in both exact and approximate counting, underscores the value of preprocessing and decomposition techniques, and outlines future directions including certification, robust benchmarking, and enhanced replication for ongoing advancement in counting under CNF encodings.

Abstract

Modern society is full of computational challenges that rely on probabilistic reasoning, statistics, and combinatorics. Interestingly, many of these questions can be formulated by encoding them into propositional formulas and then asking for its number of models. With a growing interest in practical problem-solving for tasks that involve model counting, the community established the Model Counting (MC) Competition in fall of 2019 with its first iteration in 2020. The competition aims at advancing applications, identifying challenging benchmarks, fostering new solver development, and enhancing existing solvers for model counting problems and their variants. The first iteration, brought together various researchers, identified challenges, and inspired numerous new applications. In this paper, we present a comprehensive overview of the 2021-2023 iterations of the Model Counting Competition. We detail its execution and outcomes. The competition comprised four tracks, each focusing on a different variant of the model counting problem. The first track centered on the model counting problem (MC), which seeks the count of models for a given propositional formula. The second track challenged developers to submit programs capable of solving the weighted model counting problem (WMC). The third track was dedicated to projected model counting (PMC). Finally, we initiated a track that combined projected and weighted model counting (PWMC). The competition continued with a high level of participation, with seven to nine solvers submitted in various different version and based on quite diverging techniques.

Paper Structure

This paper contains 76 sections, 10 equations, 1 figure, 10 tables.

Table of Contents

  1. Introduction
  2. Goals of the Competition
  3. Competition Tracks and Computational Complexity
  4. Contributions
  5. Related Works
  6. Solvers
  7. Preliminaries and Background
  8. Background
  9. Basics
  10. Satisfiability
  11. Models and Counting
  12. Competition Tracks
  13. Accuracy, Precision, and Outputs
  14. Restrictions, Measure, and Ranking
  15. Measuring
  16. ...and 61 more sections

Figures (1)

  • Figure 1: 2023 Iteration Track 1 (MC). Runtime results illustrated as cumulated solved instances. The y-axis labels consecutive integers that identify instances. The x-axis depicts the runtime. The instances are ordered by running time, individually for each solver.