On first-order model checking parameterized by the number of variables

Abstract

The first-order (FO) model checking problem asks, given an FO sentence $\varphi$ and a graph $G$, whether $G$ is a model of $\varphi$. This problem is $\mathsf{AW}[\ast ]$-hard when parameterized by the quantifier rank of the formula. A classical algorithm decides this problem in $\mathsf{XP}$ time when parameterized by the number of variable names in the formula. This $\mathsf{AW}[\ast ]$-hardness motivates study of the problem on well-behaved graph classes. Many results identify graph classes $\mathcal{C}$ such that the FO model checking problem restricted to $\mathcal{C}$ admits an $\mathsf{FPT}$ time algorithm when parameterized by the quantifier rank of the formula. Parameterization by the number of variable names is significantly more restrictive than parameterization by the quantifier rank, as the number of variable names can be arbitrarily small relative to the quantifier rank. We study the graph classes $\mathcal{C}$ for which the FO model checking problem restricted to $\mathcal{C}$ admits an $\mathsf{FPT}$ time algorithm when parameterized by the number of variable names in the formula. We characterize these classes in the monotone setting, and prove a slightly weaker result in the hereditary setting.