מירב זהבי

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 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).