Model Counting Competition 2024
The competition will be co-located with the competitions at SAT 2024.
Pragmatics of SAT features a Competition Solver Description Track in 2024.
The Workshop on Counting, Sampling, and Synthesis 2024 also invites solver presentations.
Tracks / Challenges
- Model Counting (mc)
- Weighted Model Counting (wmc)
- Projected Model Counting (pmc)
- Projected Weighted Model Counting (pwmc)
Results
Rules
Ranking
- A. Exact (arbitrary precision)
- B. Exact (small precision loss)
- C. Approximate (provide approximation guarantee)
- D. Heuristic (experimental)
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 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
- Track 1
- Track 2 (no negative weights, only weights w_l + w_{\neg l} = 1 or none)
- Track 2 Bonus (including negative weights) Updated Format Description (Defaults for negative weights)
- Track 3
- Track 4
Submission
Register an Account with StarExec. We will give you access and you will be able to upload your solver there. Also, please register in this form.
Format
We refer to a comprehensive document on the description of the competition format from 2021 (Updated June 2024).
Important Dates (Tentative)
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
- Martin Gebser (AAU Klagenfurt, Austria)
Technical and Reproducibility Advisor
- Daniel Le Berre
Call for Benchmarks (Over)
Model Counting Competition invites extended submissions of collections of counting instances in the an DIMACS-like submission format as used in the 2021 competition.