Best $\Pi_k \text{SAT}$ running time?

Question

Define $\Pi_k \text{SAT}$ by 'Given a quantified boolean formula $\varphi = \forall y_1\exists y_2\dots Q_ky_k\mbox{ }\phi(y_1, \dots, y_k)$, where $\phi(y_1, \dots, y_k)$ is boolean predicate with each $y_i$ a vector of variables, $Q_{2j-1} = \forall$ and $Q_{2j} = \exists$ at every $j\in\mathbb N$, is $\varphi$ valid?' (page $99$ in Arora book).

$ETH$ says $\text{SAT}$ and so $\Pi_1\text{SAT}=\overline{\text{SAT}}$ needs $\Omega(2^{c\cdot n_1})$ time at some $c>0$ where $n_1$ is number of variables in $y_1$.

If there are $n=n_1+\dots+n_k$ variables where each $y_i$ has $n_i$ variables then

1. what is the best known algorithm for $\Pi_k \text{SAT}$ at each fixed $k$?

2. Is there a generalized $ETH$ that applies to $\Pi_k\text{SAT}$?

Answer 1

These questions are discussed in detail in the paper

Rahul Santhanam, Ryan Williams:
"Beating Exhaustive Search for Quantified Boolean Formulas and Connections to Circuit Complexity"
Electronic Colloquium on Computational Complexity (ECCC) 2013, #108
https://eccc.weizmann.ac.il/report/2013/108/