Model Counting Competition 2025
The competition will be co-located with the competitions at SAT 2025.
Pragmatics of SAT invites Competition Solver Description Track.
The Workshop on Counting, Sampling, and Synthesis 2025 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 (tbd)
- Track 6B: Bitvector Counting
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 and 6 are bonus tracks, which will be experimental and run in collaboration with the solver developers.
Results
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)
Benchmark Selection
We precompute instances and discard those that can be solved by standard solvers within less than 10s and keep at most 40 instances that cannot be solved by common existing solver.
Public Instances
tbd
Submission
Please register in this form.
Format
We refer to a comprehensive document on the description of the competition format from 2021 (Updated June 2024) for Tracks 1-4.
Note that weights may be given as rational number either as decimal number with at most 9 significant digits or as fraction.
For Track 5, we will decide about the format after discussing with interested developers (please send us an email).
For Track 6, we use the SMT format.
Important Dates
Refer to the submission and important dates page.
Organization
Program Co-Chair / Organization
- Arijit Shaw (Chennai Mathematical Institute, India)
- Markus Hecher (MIT, MA, United States)
- Johannes K. Fichte (Linköping University, Sweden)
Judge
tba
Technical and Reproducibility Advisor
tba
Call for Benchmarks
Model Counting Competition invites extended submissions of collections of counting instances in the an DIMACS-like submission format (updated June’24). See: details
Evaluation Plattform
We are happy that the https://www.sosy-lab.org/ accepted to host the model counting competition. Thank you Dirk Beyer and Philipp Wendler.
Pre-valuation will be run at the Swedish National Supercomputer Centre (NSC) and the
https://www.nsc.liu.se/systems/tetralith/.
(Note that StarExec Iowa is about to be decommissioned in 2025).
Submission will require a private github repository (or similar), from where we can pull the solvers.