Fine-Grained Bounds for Courcelle's Theorem

Courcelle's theorem states that there exists an algorithm that takes as input a graph G of treewidth at most t and a MSO formula ϕ, and determines whether G satisfies ϕ in time f (ϕ, t) • n. It is folklore that the the function f contains a tower of exponentials whose height depends as a linear function of the number of quantifier alternations of the input formula ϕ. A classic reduction of Frick and Grohe shows that, assuming the Exponential Time Hypothesis (ETH), the linear growth of the height of the tower is unavoidable. Nevertheless, there is still a huge gap between existing upper and lower bounds -after all, there is quite a difference between a single exponential and a double exponential running time. In addition, this only gives us a very coarse understanding in the time complexity of Courcelle's theorem. In this paper, we prove a fine-grained version of Courcelle's theorem with nearly ETH-tight dependence on the treewidth parameter t and the quantifier structure of ϕ (specifically, the number of first order and second order variables in each quantifier alternation block).