MC 2020

Thanks for participating. Hope to see you in 2021.

Updated results are available Download Updated Slides.

For details on the workshop its presentations, slides, and recordings we refer to the Programm.

Updated results of the competition will be out soon.

MC 2020 (Model Counting 2020)

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.

Further details on the competition can be found at: Competition (MC 2020)

MCW 2020 (Workshop on Model Counting)

The International Workshop on Model Counting (MCW 2020) aims to provide a venue for researchers working on model counting such as model counting (mc), weighted model counting/sum of products (wmc), projected model counting (pmc) within the realm but not restricting to Boolean satisfiability (SAT), satisfiability modulo theories (SMT), Answer set programming (ASP), and constraint programming (CP). It encourages to meet, communicate, and discuss the latest theoretical and practical results, in particular results on novel solvers, related solver technologies, new theoretical advances, practical academic and industrial applications as well as the linking theory and practice. The workshop is also the place for developers of model counters to present their solvers and the presentation of detailed results on the model counting competition.

Further details on the competition can be found at: Workshop (MCW 2020@SAT)


For competition and workshop submissions see Dates and Submission for MC2020 & MCW 2020@SAT.


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.

Beside the theoretical research there are many implementations available, just to name some state of the art solvers, c2d, d4, DSHARP, miniC2D, cnf2eadt, bdd_minisat_all, and sdd (based on knowledge compilation techniques); ApproxMC4, and sts (based on approximate counting or sampling); ganak (probabilistic exact counting); Cache, sharpCDCL4, and sharpSAT (CDCL-based solvers using component caching); gpusat, countAntom, and dCountAntom) (parallel or distributed solvers). There are also preprocessors available B+E and pmc. Many solvers are highly competitive and solve various instances. However, there has still not been a competition on the topics related to model counting.


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.