Faster decision of first-order graph properties

ABSTRACT. First-order logic captures a vast number of computational problems on graphs. We study the time complexity of deciding graph properties definable by first-order sentences with $k$ variables. The trivial algorithm for this problem runs in $O(n^k)$ time on $n$-node graphs (the big-O hides the dependence on $k$).

Answering a question of Miki Ajtai, we give the first algorithms running faster than the trivial algorithm, in the general case of arbitrary first-order sentences and arbitrary graphs. One algorithm runs in $O(n^{k-3+\omega)} \leq O(n^{k-0.627})$ time for all $k \geq 3$, where $\omega < 2.373$ is the $n \times n$ matrix multiplication exponent. By applying fast rectangular matrix multiplication, the algorithm can be improved further to run in $O(n^{k-1+o(1)})$ time, for all $k \geq 9$. Finally, we observe that the exponent of $k-1$ is optimal, under the hypothesis that CNF satisfiability with $n$ variables and $m$ clauses cannot be solved in $(2-\epsilon)^n \cdot \poly(m)$ time for some $\epsilon > 0$.