Parameterized complexity investigations on the first-order satisfiability and matching problems

Abstract

Parameterized complexity theory is a subarea of computational complexity theory in which the run-time analysis of a computational problem handles, besides the input size, an additional term that allows us to recognize “some kind of tractability” for many previously intractable problems. Many problems from Logic have been received attention by some parameterized analysis technique. We explore two logical tasks using the tools of the parameterized complexity. First, we study the parameterized complexity of the satisfiability problem for some prefix-vocabulary fragments of first-order logic. We consider the natural parameters emerging from the definition of these fragments, such as the quantifier rank, and the number of relation symbols. Following the classical classification of decidable prefix-vocabulary fragments, we observed that, when combining with the finite model property, many fragments have fixed-parameter tractability for the satisfiability concerning some of these parameters. Secondly, we apply parameterized complexity theory for classification for associative, commutative, and associative-commutative matching problems ({A, C, AC}-MATCHING) considering different parameterizations. We primarily consider the number of variables, the size of the substitution, and the size of the vocabulary as parameters. Combining the size of the substitution and the size of the vocabulary, we established the fixed-parameter tractability for these matching problems. For the other cases, we obtained the membership in W[P] for C-MATCHING for the number of variables and, for {A, AC}-MATCHING, when considering the size of the substitution.