2021/04/21 by Alexsander A. de Melo, Alexsander Andrade de Melo, de Melo, Alexsander Andrade +2
Computer Science · #Advanced Algebra and Logic #Advanced Graph Theory Research #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #cs.LO #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.2104.10286
A preliminary version of this work was published in the proceedings of the 27th International Conference on Automated Deduction
arxiv created 2021/04/21 · openalex publication_date 2021/04/21 · arxiv updated 2021/04/22 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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 ψ over a vocabulary τ, and a finite automaton F over a suitable alphabet B(Σ,w,τ) representing a width-w regular-decisional class of τ-structures C, one can decide in time f(τ,Σ,ψ,w)|F| whether some τ-structure in C satisfies ψ. Here, f is a function that depends on the parameters τ,Σ,ψ,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 τ, ψ, Σ 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.