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

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.

• Call for Benchmarks 2024 (TEXT)

Rules

Ranking

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

Restictions

• 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.

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.

Important Dates (Tentative)

• Feb 11: Call for Benchmarks, Participation
• Mar 30 Apr 9: Benchmark Submission Deadline
• Apr 30: Public Instance Publication
• May 30: Solver Submission Deadline
• Jun 30: Notification of public results
• Jul 15: Notification of private results
• Jul 30: Comments Deadline by Participants
• Aug 24: Result Declaration at SAT Conf.

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