| Title | : | Counting winning strategies in two player games: Theory and Practice |
| Speaker | : | Vaibhav Krishan (IIT Madras) |
| Details | : | Tue, Oct 13, 2026 4:00 PM, @ SSB 334 |
| Abstract | : | Quantified Boolean Formulas (QBFs) can be viewed as two-player games: the players alternately assign Boolean values to variables, with one player trying to satisfy a given propositional formula and the other trying to falsify it. The QBF problem asks whether the first player has a winning strategy. In this talk, we ask a more quantitative question: how many winning strategies are there? This question introduces challenges that do not arise in ordinary solution counting. A strategy may depend on the opponents previous moves, the space of strategies can be enormous, and the number of winning strategies itself can be doubly exponential in the size of the formula. At the same time, QBF and its variants provide a natural language for reasoning about adversarial choices and unknown environments, with applications including formal verification, planning, reactive synthesis, and model checking. I will discuss both theoretical and practical approaches to counting winning strategies in QBFs. I will describe a solver we have developed that exploits the structure of the underlying strategy space to avoid explicitly exploring or representing it in full. I will then discuss the theoretical foundations behind these techniques and how they suggest stronger methods for future solvers. More broadly, the talk will illustrate an interplay between theory and practice: theoretical structure leads to practical algorithms, while computational considerations motivate new theoretical questions. This talk is based on joint work with Sravanthi Chede and Anil Shukla (FSTTCS 2026, to appear), and with Sravanthi Chede, Leroy Chew, and Anil Shukla (SAT 2026). Speaker Bio: Vaibhav is a post doctoral researcher in the CSE department at IIT Madras. Previously, he was a post doctoral fellow in the TCS group at IMSc, Chennai. He received his PhD in CSE from IIT Bombay, where he was advised by Prof. Nutan Limaye and Prof. Sundar Vishwanathan. His research interests lie broadly in complexity theory and automated reasoning, with a focus on understanding computational hardness from both theoretical and practical perspectives. Apart from his academic career, he has spent more than five years in industry as a quantitative trader. |