19 October 2020 – Members from Meel Group (Sung Kah Kay Assistant Professor Kuldeep S. Meel’s research lab) emerged champions at the 1st International Competition on Model Counting (MC 2020). A total of 17 entries were submitted to this year’s competition, which aimed to evaluate the performance of model counting tools.
Model counting problems aim to estimate the number of possible assignments that satisfy a given set of constraints. For example, if the constraints are (1) ‘a person who likes durian’ and (2) ‘a person who lives in Singapore’, then the model counting problem is to count the number of people who live Singapore, and like durian.
Dr Meel and Visiting Senior Research Fellow Mate Soos teamed up with Dr Subhajit Roy, an Associate Professor at the Indian Institute of Technology Kanpur, and Shubham Sharma, a former student of both Dr Meel and Dr Roy.
They developed an approximate model counter, ApproxMC, which counts by partitioning the entire space of assignments into small cells, thereby taking advantage of the highly sophisticated heuristics used in modern SAT solvers. This is complemented by GANAK, a tool they created for counting exact models.
“Our work stood out because of this sophisticated hybrid approach using self-developed tools for both exact and approximate model counting. These two tools worked together, taking advantage of their respective strengths, to win the competition,” said Dr Meel.
“We have put much effort into both the theoretical understanding and the practical runtime analysis of the system, improving both sides at the same time. This led to the development of a strong, highly competitive, easy-to-use system,” added Dr Soos.
“Our system is built on the algorithmic framework that has been in development for over 8 years with collaborators across the world, and in particular, it is important to acknowledge our co-authors on the first two versions of ApproxMC, Prof Supratik Chakraborty (IIT Bombay), and Prof Moshe Vardi (Rice University),” said Dr Meel.
“We are also indebted to the team at the National Supercomputing Centre Singapore for their generous access to the supercomputing cluster, which has allowed us to develop an in-depth understanding of performance bottlenecks,” he added.
