【作者】 王旌阳；

【导师】 傅育熙；

【作者基本信息】 上海交通大学 ， 计算机软件与理论， 2010， 硕士

【摘要】 对于一种逻辑(?),它在一类结构C上的模型检测问题是询问一个给定的(?)语句在一个给定的C结构中是否成立。核化是一个在设计固定参数算法中广泛应用的技术。核是一个从输入实例中计算并输出同一个问题的等价实例的多项式算法,而且要求输出实例的大小和参数都是输入实例参数的函数。本文中,我们通过核化技术研究一些一阶逻辑子逻辑(通过限定一阶逻辑的布尔连接词和量词得到的逻辑)的模型检测问题的参数复杂性。本文中引用了最近提出的蒸馏机制。首先我们证明了正存在式一阶逻辑在二分图上的参数模型检测问题存在线性核,其中参数为输入语句的长度。其次,在相同的参数情况下,我们证明了存在式一阶逻辑在路径上的参数模型检测问题有线性核。最后,在的假设下,对于固定的结构,我们证明了存在式或全称式一阶逻辑的参数模型检测问题没有多项式核,此时的参数为语句中的变元个数。更多还原

【Abstract】 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.更多还原