Tata Institute of Fundamental Research
A Theory for Computing with SAT Solvers: What's the Power of a Satisfying Assignment?
STCS Seminar
Speaker:
Kuldeep Meel (Georgia Institute of Technology)
Organiser:
Shibashis Guha
Date:
Thursday, 17 Jul 2025, 11:00 to 12:00
Venue:
A-201 (STCS Seminar Room)
(Scan to add to calendar)
Abstract:
The past two decades have witnessed dramatic improvements in SAT solving, enabling today's solvers to handle problems involving millions of variables. Motivated by the power of SAT solvers, there is a growing interest in tackling problems that lie in higher classes of the polynomial hierarchy, wherein NP calls are to be replaced by SAT solvers in practice. The complexity of such algorithms is measured in terms of calls to NP oracles. However, SAT solvers are not mere decision oracles: they also provide a satisfying assignment when the formula is satisfiable. Therefore, a theory based on NP oracles is limiting, and there is a need for a theory that takes into account the power of SAT solvers. In this talk, I will discuss how such consideration leads to new algorithms and new lower bounds in the context of two fundamental problems: model counting and sampling.
Based on joint work (LICS-22 and ICALP-23) with Diptarka Chakaraborty, Sourav Chakraborty, Remi Delannoy, and Gunjan Kumar.
Short 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.
| Speaker: | Kuldeep Meel (Georgia Institute of Technology) |
| Organiser: | Shibashis Guha |
| Date: | Thursday, 17 Jul 2025, 11:00 to 12:00 |
| Venue: | A-201 (STCS Seminar Room) |
(Scan to add to calendar)
The past two decades have witnessed dramatic improvements in SAT solving, enabling today's solvers to handle problems involving millions of variables. Motivated by the power of SAT solvers, there is a growing interest in tackling problems that lie in higher classes of the polynomial hierarchy, wherein NP calls are to be replaced by SAT solvers in practice. The complexity of such algorithms is measured in terms of calls to NP oracles. However, SAT solvers are not mere decision oracles: they also provide a satisfying assignment when the formula is satisfiable. Therefore, a theory based on NP oracles is limiting, and there is a need for a theory that takes into account the power of SAT solvers. In this talk, I will discuss how such consideration leads to new algorithms and new lower bounds in the context of two fundamental problems: model counting and sampling.
Based on joint work (LICS-22 and ICALP-23) with Diptarka Chakaraborty, Sourav Chakraborty, Remi Delannoy, and Gunjan Kumar.
Short 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.