Abstract
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 $\phi$, and determines whether $G$ satisfies $\phi$ in time $f(\phi,t) \cdot n$. It is folklore that the function $f$ contains a tower of exponentials whose height depends linearly on the number of quantifier alternations of the input formula $\phi$. A classic reduction by Frick and Grohe shows that, assuming the Exponential Time Hypothesis (ETH), the linear growth of the height of the tower is unavoidable.
Nevertheless, there remains a significant gap between existing upper and lower bounds—there is a substantial difference between a single exponential and a double exponential running time. Furthermore, this only provides a very coarse understanding of 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 $\phi$ (specifically, the number of first-order and second-order variables in each quantifier alternation block).
Blogger's Review: This study not only fills a theoretical gap in Courcelle's theorem but also brings new insights into graph theory and computational complexity. The refined time complexity analysis will drive optimizations in related algorithms, holding significant academic value and application prospects.