The 1st International Competition on Model Counting (MC 2020) is a competition to deepen the relationship between latest theoretical and practical development on the various model counting problems and their practical applications. It targets the problem of counting the number of models of a Boolean formula.

MC 2020 aims to identify new challenging benchmarks and to promote new solvers for the problem as well as to compare them with state-of-the-art solvers. The MC 2020 follows a direction in the community of constraint solving, where already many competitions have been organized such as on ASP (7 editions), CSP (19 editions), SAT (19 editions), SMT (14 editions), MaxSAT Evaluation (13 editions), QBF (8 editions).


Program Co-Chair

  • Markus Hecher (TU Wien, Vienna)
  • Johannes K. Fichte (TU Dresden, Dresden)


  • Florim Hamiti (TU Dresden, Dresden)

Scientific Partners

  • Adnan Darwiche (University of California at Los Angeles)
  • Arthur Choi (University of California at Los Angeles)
  • Armin Biere (Johannes Kepler Universitat Linz)
  • Kuldeep S. Meel (National University of Singapore)
  • Markus Hecher (TU Wien)
  • Johannes K. Fichte (TU Dresden)
  • Marijn Heule (Carnegie Mellon University)
  • Norbert Manthey (Amazon AWS Dresden)
  • Stefan Mengel (CNRS at Centre de Recherche en Informatique de Lens)
  • Pierre Marquis (CNRS at Centre de Recherche en Informatique de Lens and Université d’Artois)
  • Fahim Bacchus (University of Toronto)
  • Vibhav Gogate (University of Texas at Dallas)

Evaluation Plattform /

  • Szymon Wasik (Poznan University of Technology, Poznan)

Important Dates

  • December 18th, 2019: Announcement of the challenge (Tracks)
  • January 22nd, 2019: Call for Benchmarks
  • March 5th, 2020 (AoE) – Deadline – Benchmark Submission
  • May 22th, 2020 (AoE) – Deadline (DS) – Submission
  • June 3rd, 2020 (AoE) – Deadline (DD) – Submission of a solver description via Easychair