Beating Brute Force Search for QBF Satisfiability, and Implications for Formula Size Lower Bounds

Speaker: 

Rahul Santhanam

Affiliation: 

University of Edinburgh
School of Informatics
10, Crichton Street
Edinburgh - EH8 9AB
United Kingdom

Time: 

Thursday, 17 April 2014, 16:00 to 17:00

Venue: 

Organisers: 

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).