On the Width of Regular Classes of Finite Structures

TL;DR

This paper introduces the concept of decisional width for finite structures and regular classes, providing a decision procedure for first-order properties that is efficient when parameters are fixed.

Contribution

It defines decisional width for structures and classes, and proves decidability and fixed-parameter tractability results for first-order logic over these classes.

Findings

Decidability of first-order theory for regular-decisional classes.

Linear-time decision procedure when parameters are fixed.

Fixed-parameter tractability for counting satisfying assignments.

Abstract

In this work, we introduce the notion of decisional width of a finite relational structure and the notion of decisional width of a regular class of finite structures. Our main result states that given a first-order formula {\psi} over a vocabulary {\tau}, and a finite automaton F over a suitable alphabet B({\Sigma},w,{\tau}) representing a width-w regular-decisional class of {\tau}-structures C, one can decide in time f({\tau},{\Sigma},{\psi},w)|F| whether some {\tau}-structure in C satisfies {\psi}. Here, f is a function that depends on the parameters {\tau},{\Sigma},{\psi},w, but not on the size of the automaton F representing the class. Therefore, besides implying that the first-order theory of any given regular-decisional class of finite structures is decidable, it also implies that when the parameters {\tau}, {\psi}, {\Sigma} and w are fixed, decidability can be achieved in linear time on the size of the input automaton F. Building on the proof of our main result, we show that the problem of counting satisfying assignments for a first-order logic formula in a given structure A of width w is fixed-parameter tractable with respect to w, and can be solved in quadratic time on the length of the input representation of A.