English

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

Logic in Computer Science 2026-04-27 v1

Abstract

The first-order (FO) model checking problem asks, given an FO sentence ϕ\phi and a graph GG, whether GG is a model of ϕ\phi. This problem is known to be AW[]\mathsf{AW[*]}-hard when parameterized by the quantifier rank of the formula. A classical algorithm decides this problem in XP-time parameterized by the number of variables in the formula. Due to AW[]\mathsf{AW[*]}-hardness, it is natural to ask about the complexity of the problem when restricted to some well-behaved class of graphs. There are many results describing graph classes C\mathcal{C} such that the FO model checking problem restricted to C\mathcal{C} admits an FPT\mathsf{FPT}-time algorithm when parameterized by the quantifier rank of the formula. Parameterization by the quantifier rank is significantly more restrictive than parameterization by the number of variables. We investigate the graph classes C\mathcal{C} for which the FO model checking problem restricted to C\mathcal{C} admits an FPT\mathsf{FPT}-time algorithm when parameterized by the number of variables in the formula. We characterize these classes in the monotone setting, and prove a slightly weaker result in the hereditary setting.

Keywords

Cite

@article{arxiv.2604.22493,
  title  = {On first-order model checking parameterized by the number of variables},
  author = {Jan Jedelský},
  journal= {arXiv preprint arXiv:2604.22493},
  year   = {2026}
}
R2 v1 2026-07-01T12:33:45.296Z