Seminars

View all Seminars  |  Download ICal for this event

A Theory for Computing with SAT Solvers: Whats the Power of a Satisfying Assignment?

Series: Bangalore Theory Seminars

Speaker: Kuldeep Meel, Georgia Institute of Technology

Date/Time: Apr 07 17:00:00

Location: CSA Auditorium, (Room No. 104, Ground Floor)

Abstract:
The past two decades have witnessed dramatic improvements in SAT solving, enabling todays 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


Microsoft teams link:

Link


We are grateful to the Kirani family (Link and the Walmart Center for Tech Excellence (Link for generously supporting this seminar series


Hosts: Rameesh Paul, KVN Sreenivas, Rahul Madhavan, Debajyoti Kar, Nirjhar Das