Kernelization For First-order Model-checking Problems

The model-checking problem for a logic L on a class C of structures asks whether a given L-sentence holds in a given structure of C. Kernelization is a widely used technique to design fixed-parameter algorithms. A kernelization is a polynomial time algorithm that computes from a given instance an equivalent instance of the same problem, with the size and parameter of the output bounded by a function of the parameter of the input. In this thesis, we study the parameterized complexity of model-checking problems over some fragments of first-order logic (derived by restricting the boolean connectives and quantifiers we permit) through kernelization.A recent developed machinery named distillation is discussed in this work. First, we show that parameterized model-checking problem for existential positive first-order logic on bipartite graphs parameterized by the length of the input sentence has a linear kernelization. Second, we show that first-order model-checking problems parameterized by the length of input formula on paths have linear kernelizations. Third, conditioned on PH≠∑3P, for fixed structures, we give polynomial lower-bounds on kernelization sizes of parameterized model-checking problems for existential and universal first-order logic parameterized by the number of variables occurring in the sentence.