GET IN TOUCH
MC 2025

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.