Campus Event Calendar

AG 1

AG Audience

English

Note: We use this to send email in the morning.

30 Minutes

Saarbrücken

An important class of problems in logics and database theory is given by fixing a first-order property $\psi$ over a relational structure, and considering the model-checking problem for $\psi$. Recently, Gao, Impagliazzo, Kolokolova, and Williams (SODA 2017) identified this class as fundamental for the theory of fine-grained complexity in P, by showing that the \emph{(Sparse) Orthogonal Vectors} problem is complete for this class under fine-grained reductions. This raises the question whether fine-grained complexity can yield a precise understanding of all first-order model-checking problems. Specifically, can we determine, for any fixed first-order property $\psi$, the exponent of the optimal running time $O(m^{c_\psi})$, where $m$ denotes the number of tuples in the relational structure?

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.

Nick Fischer

Nick Fischer, 07/08/2019 02:39 PM -- Created document.