ON THE PARAMETERIZED INTRACTABILITY OF MONADIC SECOND-ORDER LOGIC

作     者：Kreutzer, Stephan 

作者机构：Tech Univ Berlin Sch Elect Engn & Comp Sci D-10587 Berlin Germany 

出 版 物：《LOGICAL METHODS IN COMPUTER SCIENCE》 (Log. Methods Comp. Sci.)

年 卷 期：2012年第8卷第1期

核心收录：

学科分类：08[工学] 0701[理学-数学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：DFG [KR 2898/1-3] 

主　　题：Parameterized Complexity Algorithmic Meta-Theorems Finite Model Theory 

摘      要：One of Courcelle s celebrated results states that if C is a class of graphs of bounded tree-width, then model-checking for monadic second order logic (MSO2) is fixed-parameter tractable (fpt) on C by linear time parameterized algorithms, where the parameter is the tree-width plus the size of the formula. An immediate question is whether this is best possible or whether the result can be extended to classes of unbounded tree-width. In this paper we show that in terms of tree-width, the theorem cannot be extended much further. More specifically, we show that if C is a class of graphs which is closed under colourings and satisfies certain constructibility conditions and is such that the tree-width of C is not bounded by log(84) n then MSO2-model checking is not fpt unless Sat can be solved in sub-exponential time. If the tree-width of C is not poly-logarithmically bounded, then MSO2-model checking is not fpt unless all problems in the polynomial-time hierarchy can be solved in sub-exponential time.