Event calendar file
School of Technology and Computer Science Seminars
Beating Brute Force Search for QBF Satisfiability, and Implications for Formula Size Lower Bounds
by Dr. Rahul Santhanam (University of Edinburgh, United Kingdom)
Thursday, April 17, 2014
from
to
(Asia/Kolkata)
at Colaba Campus ( AG-80 )
at Colaba Campus ( AG-80 )
| Description |
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).
|
