GET IN TOUCH
MC 2020

MC 2020 (Model Counting 2020)

How to use Optil.io?

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
    Download Public Instances (available now: 2020-04-21); Download Private Instances (available now: 2020-07-13); Download All Instances (available now: 2020-07-13);

  2. Weighted Model Counting (wmc) (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
    Download Public Instances (Updated: 2020-05-03); Download Private Instances (available now: 2020-07-13); Download All Instances (available now: 2020-07-13);

  3. Projected Model Counting (pmc) (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 (TBA)
    Download Public Instances (available now: 2020-06-03); Download Private Instances (available now: 2020-07-13);

Competition

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.

Background

The success of solver technologies for declarative languages, such as SAT, in the last two decades is mainly due to both the availability of numerous efficient solver implementations and to the growing number of problems that can efficiently be solved through the declarative approach. Designing efficient solvers requires both understanding of the fundamental algorithms underlying the solvers, as well as in-depth insights into how to implement the algorithms for obtaining efficient and robust solvers.

Several competitive events are regularly organized for different declarative solving paradignms, including SAT competitions QBF evaluations, MaxSAT evaluations, SMT, ASP and CP competitions, etc., to evaluate available solvers on a wide range of problems. The winners of such events set regularly new standards in the area. If the systems themselves are widely spread, many details on their design or in their implementation can only be found in the source code of the systems.

The aim of the workshop is to allow researchers to share both fundamental theoretical insights into practical solvers, as well as new implementation-level insights and ‘gory’ technical details about their systems that may at times be difficult to publish in the main conferences on the declarative solving paradigms.

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

For competition details, we refer to the Submission Information.

Model Counting

Model counting is very vibrant field that provided both recent advances in theory as well as in practical solving including various applications. State-of-the-art SAT or WMC (weighted model counting) search engines so far rely on standard techniques from SAT-based solving, knowledge compilation, or approximate solving by means of sampling using SAT solvers. There have been also successful implementations for parallel and distributed computation as well as massively parallel computation approaches.

For further details on the problem, we refer to the page on model counting.


Organization

Program Co-Chair

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

Student

  • 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
  • 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 / optil.io

Szymon Wasik (Poznan University of Technology, Poznan)

Sponsors

On behalf of the Program Committee of MC 2020, we invite you to participate in the sponsoring of metals and travel support for the winners.

data-experts already announced sponsoring for MC 2020.

data-experts