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 1F: Model Counting (same instances, timeout of 120s)
- Track 2B: Weighted Model Counting (New instances with negative weights in 2026)
- Track 3: Projected Model Counting
- Track 4: Projected Weighted Model Counting (Mixed instances, wmc,pmc,pwmc)
- Track 5B: Algebraic Model Counting (AMC): Field (complex numbers)
Tracks 1F, 2B, 5B are bonus track, which will be experimental.
Submission
See submission instructions for details.
- Please register in this form (Benchmark Submissions)
- Please register in this form (Solver Submissions)
Results
- Presenting at SAT2026 (Thursday 13:30 on 23 July). Link to the Program
- Special Awards during the FLoC Banquet
Public Instances
- Instances for Track 1,3 (last updated June 6, 2026)
- Instances for Track 2B, 4, 5 (last updated June 28, 2026)
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
Call for Benchmarks
Model Counting Competition invites extended submissions of collections of counting instances in the an DIMACS-like submission format. See: details
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.