Tata Institute of Fundamental Research
Beating Brute Force Search for QBF Satisfiability, and Implications for Formula Size Lower Bounds
Seminar
Speaker:
Rahul Santhanam (University of Edinburgh
School of Informatics
10, Crichton Street
Edinburgh - EH8 9AB
United Kingdom)
Organiser:
Arkadev Chattopadhyay
Date:
Thursday, 17 Apr 2014, 16:00 to 17:00
Venue:
AG-80
(Scan to add to calendar)
Abstract:
Abstract: We give the first algorithms for the QBF Satisfiability problem beating brute force search. We show that the QBF satisfiability question for CNF instances with $n$ variables, $q$ quantifier blocks and size $poly(n)$ can be solved in time $2^{n-\Omega(n^{1/(q+1)})}$, and that the QBF satisfiability question for circuit instances with $n$ variables, $q$ quantifier blocks and size $poly(n)$ can be solved in time $2^{n-\Omega(q)}$. We also show that improvements on these algorithms would lead to super-polynomial formula size lower bounds for NEXP (this is joint work with Ryan Williams).
| Speaker: | Rahul Santhanam (University of Edinburgh School of Informatics 10, Crichton Street Edinburgh - EH8 9AB United Kingdom) |
| Organiser: | Arkadev Chattopadhyay |
| Date: | Thursday, 17 Apr 2014, 16:00 to 17:00 |
| Venue: | AG-80 |
(Scan to add to calendar)
Abstract:
Abstract: We give the first algorithms for the QBF Satisfiability problem beating brute force search. We show that the QBF satisfiability question for CNF instances with $n$ variables, $q$ quantifier blocks and size $poly(n)$ can be solved in time $2^{n-\Omega(n^{1/(q+1)})}$, and that the QBF satisfiability question for circuit instances with $n$ variables, $q$ quantifier blocks and size $poly(n)$ can be solved in time $2^{n-\Omega(q)}$. We also show that improvements on these algorithms would lead to super-polynomial formula size lower bounds for NEXP (this is joint work with Ryan Williams).