Seminar Announcement
Date: Wednesday, 9 April 2025
Time: 2 to 3 PM
Venue: Lecture Hall 202
A Theory for Computing with SAT Solvers: What's the Power of a Satisfying Assignment?
Kuldeep Meel
Georgia Institute of Technology.
09-04-25

---

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