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
- Model Counting (mc)
- Weighted Model Counting (wmc)
- Projected Model Counting (pmc)
- 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)
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.
- Markus Hecher (TU Wien, Austria)
- Johannes K. Fichte (TU Wien, Austria)
Technical and Reproducibility Advisor
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.