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

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

• AG-80

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