Model Counting Competition 2026

The competition will be co-located with the competitions at SAT 2026.

Pragmatics of SAT invites Competition Solver Description Track.
The Workshop on Counting, Sampling, and Synthesis 2026 also invites solver presentations.

Tracks / Challenges

• Track 1: Model Counting
• Track 2: Weighted Model Counting (subsumed by Track 4)
• Track 3: Projected Model Counting
• Track 4: Projected Weighted Model Counting
• Track 5B: Algebraic Model Counting (AMC): Field (complex numbers)

Track 2: Since the results no Track 2 were quite similar to Track 4 in 2024, we omit weighted model counting unless requested by solver developer who has not been participating in the competition.

Tracks 5 is a bonus track, which will be experimental and runs in collaboration with the solver developers.

Submission

See submission instructions for details.

• Please register in this form (Benchmark Submissions)
• Please register in this form (Solver Submissions)

Public Instances

• Instances for Track 1,3 (last updated June 6, 2026)
• Tracks 2,4,5B: tbd

Rules

Ranking

• A. Exact (arbitrary precision)
• B. Exact (small precision loss)
• C. Approximate (provide approximation guarantee)
• D. Heuristic

Restrictions

• Runtime: 3600s
• Memory: 32GB
• TempDisk Space: available for input transformation and preprocessing
• Precision (in relative error A,B,D):
  • Ranking A: 0.0 (any wrong solution results in removal from the ranking)
  • Ranking B: 0.001 (more than 20 solutions outside margin results in disqualification)
  • Ranking C: $\alpha=0.8$ (more than 20 solutions outside margin results in removal from the ranking)
  • Ranking D: 20% (correct answer: 1 point, otherwise: 0 points)

A few test instances are available in the GitHub repository.

Format

We refer to a comprehensive document on the description of the competition format from 2021 (Updated June 2025 for complex weights) for Tracks 1-5.

Note that weights may be given as rational number either as decimal number with at most 9 significant digits or as fraction.

Important Dates

Refer to the submission and important dates page.

Organization

Program Co-Chair / Organization

• Arijit Shaw (Chennai Mathematical Institute, India)
• Markus Hecher (CNRS, Artois University (CRIL), France)
• Johannes K. Fichte (Linköping University, Sweden)

Judge

Mario Alviano

Technical and Reproducibility Advisor

• tbd <!–
• Daniel Le Berre –>

Call for Benchmarks

Model Counting Competition invites extended submissions of collections of counting instances in the an DIMACS-like submission format. See: details

• Call for Benchmarks 2026 (PDF)
• Call for Benchmarks 2026

Evaluation Plattform

Pre-valuation will be run at the Swedish National Supercomputer Centre (NSC) and the Tetralith Cluster.

Submission will require a private github repository (or similar), from where we can pull the solvers.