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).
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.
Szymon Wasik (Poznan University of Technology, Poznan)
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.