Title:	Propositional Model Counting
DNr:	NAISS 2024/5-323
Project Type:	NAISS Medium Compute
Principal Investigator:	Johannes Klaus Fichte <johannes.fichte@liu.se>
Affiliation:	Linköpings universitet
Duration:	2024-07-01 – 2025-07-01
Classification:	10201 10105 10103
Homepage:	https://mccompetition.org/
Keywords:

Abstract

Propositional model counting (MC), also known as number SAT or #SAT, asks to output the number of models of a propositional formula. Despite its computational hardness, the field has seen considerable advances in recent years and highly efficient solvers emerged, capable of solving larger problems each year. These solvers have immediate use in various domains, such as formal verification of hardware, software, and security protocols, combinatorial optimization, computational mathematics, or artificial intelligence in general. Over the last few years, various applications can be witnessed in the literature. Due to the increasing practical interest in counting, the Model Counting Competition (MCC) was conceived in October 2019 and four iterations have successfully carried out. The 5th iteration is planned for 2024 and will be part of the 26th International Conference on Theory and Applications of Satisfiability Testing. The competition identifies new challenging applications and benchmarks, promotes fast and reliable solvers for the problem, and provides a neutral comparison of state-of-the-art solvers. The result of the competition will be a good indicator of the current feasibility of model counting for various applications.