Algorithmic Meta-Theorems for Graphs of Bounded Vertex Cover

TL;DR

This paper improves the algorithmic complexity bounds for MSO and FO logic decision problems on graphs with bounded vertex cover, using a new graph width measure and techniques different from standard treewidth methods.

Contribution

It introduces a novel approach and a new graph width measure that significantly reduces the complexity bounds for certain graph classes, addressing an open problem.

Findings

Doubly exponential time for MSO logic on bounded vertex cover graphs

Singly exponential time for FO logic on bounded vertex cover graphs

Lower bounds show these bounds are close to optimal under complexity assumptions

Abstract

Possibly the most famous algorithmic meta-theorem is Courcelle's theorem, which states that all MSO-expressible graph properties are decidable in linear time for graphs of bounded treewidth. Unfortunately, the running time's dependence on the MSO formula describing the problem is in general a tower of exponentials of unbounded height, and there exist lower bounds proving that this cannot be improved even if we restrict ourselves to deciding FO logic on trees. In this paper we attempt to circumvent these lower bounds by focusing on a subclass of bounded treewidth graphs, the graphs of bounded vertex cover. By using a technique different from the standard decomposition and dynamic programming technique of treewidth we prove that in this case the running time implied by Courcelle's theorem can be improved dramatically, from non-elementary to doubly and singly exponential for MSO and FO logic respectively. Our technique relies on a new graph width measure we introduce, for which we show some additional results that may indicate that it is of independent interest. We also prove lower bound results which show that our upper bounds cannot be improved significantly, under widely believed complexity assumptions. Our work answers an open problem posed by Michael Fellows.