Model Counting Competition 2025

The competition will be co-located with the competitions at SAT 2025 (expected).

Tracks / Challenges

1. Model Counting (mc)
   
2. …
3. tba

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

Submission

Please register in this form.

TBD

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

tba

Technical and Reproducibility Advisor

tba

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.

• Call for Benchmarks 2024 (TEXT)