A Fine-Grained Analogue of Schaefer's Theorem in P: Dichotomy of Exists^k Forall-Quantified First-Order Graph Properties

Towards answering this question, in this work we give a dichotomy for the class of $\exists^k \forall$-quantified graph properties. For every such property $\psi$, we either give a polynomial-time improvement over the baseline $O(m^k)$-time algorithm or show that it requires time $m^{k-o(1)}$ under the hypothesis that MAX3SAT has no $O((2-\epsilon)^n)$-time algorithm. More precisely, we define a hardness parameter $h = H(\psi)$ such that $\psi$ can be decided in time $O(m^{k-\epsilon})$ if $h \le 2$ and requires time $m^{k-o(1)}$ for $h \ge 3$ unless the $h$-uniform Hyperclique hypothesis fails. This unveils a natural hardness hierarchy within first-order properties: for any $h \ge 3$, we show that there exists a $\exists^k \forall$-quantified graph property $\psi$ with hardness $H(\psi)= h$ that is solvable in time $\Order(m^{k-\epsilon})$ \emph{if and only if} the $h$-uniform Hyperclique hypothesis fails. Finally, we give more precise upper and lower bounds for an exemplary class of formulas with $k = 3$ and extend our classification to a counting dichotomy.