MC 2020

Model Counting Competition: Submission Information

How to use

We refer to a more detailed subpage.

Tracks / Challenges

  1. Model Counting (mc) (Compute the number of satisfying assignments to a given CNF):
    Details for the track (Formats)
    Optil Test Submission (Lite Track / allows to test your parser etc…)
    Optil Track Submission

  2. Weighted Model Counting (wmc) (Compute the weighted model count of a given CNF and weights):
    Details for the track (Formats)
    Optil Test Submission (Lite Track / allows to test your parser etc…)
    Optil Track Submission

  3. Projected Model Counting (pmc) (Compute the projected model count of a given CNF and projection variables):
    Details for the track (Formats)
    Optil Test Submission (Lite Track / allows to test your parser etc…)
    Optil Track Submission (TBA)

Call for Benchmarks

Model Counting Competition MC 2020 invites submission of collections of (weighted) model counting instances in the standard DIMACS-based submission formats as given at the competition tracks and format.

Submission Procedure

A benchmark submission should consist of a single zip or gzipped tar package, containing the instance files and a description of the benchmarks. Please use appropriate file naming conventions, where suited. Ideally, each instance file name should contain a short descriptive part for the problem domain as well as the parameters used for generating the instance as applicable. The benchmark description must be submitted as PDF. The description should include author information with affiliations, a description of the problem domains, a description of the parameters used for generating the instances, and the file name convention. References should be used as appropriate. The benchmark descriptions will be posted on the MC 2020 website. Furthermore, the organizers are considering publishing the collection of system and benchmark descriptions on arxiv. Please submit benchmarks by email to using the subject title “MC 2020 benchmark submission” by March 5 AoE the latest.

Call for Participation


  1. Register at (
  2. Access Easychair (mc2020, and register your group
    • Use as title of the paper your login name at optil
    • Place the name of your solver in the abstract
  3. Optional: Test the formats of your solution via optil for Model Counting, Weighted Model Counting and Projected Model Counting
  4. Regularly submit your solution via optil for Model Counting and Weighted Model Counting


  1. As programming languages we plan to allow C, C++, C#, Java8, Java10, Python2, Python3, Rust, and VB.NET.
  2. Open Source (e.g. GPL, MIT, or public domain)
  3. Source code is available on a public repository (e.g., Bitbucket, GitHub, Gitlab). Note: We allow a limited use of external dependencies. These external dependencies may include commercial solvers such as IBM Cplex, gurobi, as well as open source solvers. However, please contact us in advance, since we need to get it running on
  4. Submissions Solver: Deadline (DS)
    1. Submission via
    2. Register solver and participants via EasyChair
    3. Create a release in the public repository of the solver (name: mc-2020)
  5. Submission Description: Deadline (DD)
    1. Place the source code of the solver in a digital library (e.g., Zenodo) and generate a DOI
    2. Submit solver description via EasyChair use DOI to refer to the solver and include a reference to the public source code repository

Optil System

  1. Check Optil Environment and Optil Help
  2. Optil runs on a Xenial; benchmarks are run in a docker container
  3. Restrictions/Runtime limitations:
    • Runtime: 900s (soft cpu), 905 (hard cpu), 1000 (soft wall), 1005 (hard wall)
    • Output: 524288 B
    • Mem: 8,388,608 KB


  • Content of the Repository
    • or LICENSE.txt file at the root
    • or README.txt file at the root
    • or INSTALL.txt file at the root that contains the requirements for external libraries
      • Language specific file for easy installation (e.g., CMakeLists.txt for cmake or environment.yaml for anaconda); the file is not mandatory, however, we encourage to provide it at the time of the submission of the solver description

Solver Description

  • 2+ pages
  • Should briefly describe the used techniques and references to the original publications.