The Rise of Approximate Model Counting: A Child of SAT Revolution

Title of the Talk: The Rise of Approximate Model Counting: A Child of SAT Revolution
Speakers: Prof. Kuldeep S. Meel
Host Faculty: Dr.Ashish Mishra
Date: Jul 28, 2025
Time: 11:00am to 12:00 pm
Venue: CS-LH1

Abstract: The paradigmatic NP-complete problem of Boolean satisfiability (SAT) is a central problem in Computer Science. The past 20 years have witnessed a SAT revolution with the development of conflict-driven clause-learning (CDCL) SAT solvers. Such solvers combine a classical backtracking search with a rich set of effective heuristics. While 20 years ago SAT solvers were able to solve instances with at most a few hundred variables, modern SAT solvers solve instances with up to millions of variables in a reasonable time. The SAT revolution opens up opportunities to design practical algorithms with rigorous guarantees for problems in complexity classes beyond NP by replacing a NP oracle with a SAT Solver.

In this talk, we will discuss how we use SAT revolution to design practical algorithms for one of the fundamental problems in formal methods and artificial intelligence: model counting. Model counting has applications in diverse areas spanning neural network verification, reliability estimation, explainable AI, probabilistic inference, security vulnerability analysis, and the like. While model counting has been studied extensively by theoreticians for the past three decades. Yet, in spite of this extensive study, it has been extremely difficult to reduce this theory to practice. We examine how the process of revisiting and refining the theory to leverage the SAT revolution has led to the development of the the first scalable framework for model counting: ApproxMC. ApproxMC can handle industrial-scale problem instances involving hundreds of thousands of variables, while providing provably strong approximation guarantees.

Bio: Kuldeep Meel holds Stephen Fleming Early-Career Associate Professorship in the School of Computer Science at GeorgiaTech, and an Associate Professor at the University of Toronto (on leave). His research interests lie at the intersection of Formal Methods and Artificial Intelligence. He is a recipient of the 2022 ACP Early Career Researcher Award, the 2019 NRF Fellowship for AI, and was named AI’s 10 to Watch by IEEE Intelligent Systems in 2020. His research program’s recent recognitions include the 2023 CACM Research Highlight Award, 2022 ACM SIGMOD Research Highlight, IJCAI-22 Early Career Spotlight, Distinguished Paper Award at CAV-23, “Best Papers of CAV” (2020 and 2022) special issue in FMSD journal, Best Paper Award nominations at ICCAD-21 and DATE-23, 1st Place in Model Counting Competition (2020 and 2022). He is passionate about teaching, and most proud of being recipient of university-level Annual Teaching Excellence Awards in 2022 and 2023.