MC 2023

Model Counting Competition 2023

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

Send us an email and stay tuned.

Tracks / Challenges

  1. Model Counting (mc)
  2. Weighted Model Counting (wmc)
  3. Projected Model Counting (pmc)
  4. Projected Weighted Model Counting (pwmc)

Call for Benchmarks

Model Counting Competition invites extended submissions of collections of counting instances in the an DIMACS-like submission format as used in the 2021 competition.



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


  • 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 disqualification)
    • 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 disqualification)
    • 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



Program Co-Chair

  • Markus Hecher (TU Wien, Austria)
  • Johannes K. Fichte (TU Wien, Austria)


  • tba

Technical and Reproducibility Advisor

  • Daniel Le Berre

Evaluation Plattform

We are happy that the director of StarExec (Aaron Stump, Iowa) accepted to host the model counting competition. The main part of the competition will run on StarExec. We evaluate the solvers in parallel also on the Taurus Cluster in Dresden.