The competition will be co-located with the competitions at SAT 2025.
Pragmatics of SAT invites Competition Solver Description Track.
The Workshop on Counting, Sampling, and Synthesis 2025 also invites solver presentations.
Track 2: Since the results no Track 2 were quite similar to Track 4 in 2024, we omit weighted model counting unless requested by solver developer who has not been participating in the competition.
Tracks 5 and 6 are bonus tracks, which will be experimental and run in collaboration with the solver developers.
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.
tbd
Please register in this form.
We refer to a comprehensive document on the description of the competition format from 2021 (Updated June 2024) for Tracks 1-4.
Note that weights may be given as rational number either as decimal number with at most 9 significant digits or as fraction.
For Track 5, we will decide about the format after discussing with interested developers (please send us an email).
For Track 6, we use the SMT format.
Refer to the submission and important dates page.
tba
tba
Model Counting Competition invites extended submissions of collections of counting instances in the an DIMACS-like submission format (updated June’24). See: details
We are happy that the https://www.sosy-lab.org/ accepted to host the model counting competition. Thank you Dirk Beyer and Philipp Wendler.
Pre-valuation will be run at the Swedish National Supercomputer Centre (NSC) and the
https://www.nsc.liu.se/systems/tetralith/.
(Note that StarExec Iowa is about to be decommissioned in 2025).
Submission will require a private github repository (or similar), from where we can pull the solvers.