一阶逻辑模型检测问题的核
|
摘要
对于一种逻辑(?),它在一类结构C上的模型检测问题是询问一个给定的(?)语句在一个给定的C结构中是否成立。核化是一个在设计固定参数算法中广泛应用的技术。核是一个从输入实例中计算并输出同一个问题的等价实例的多项式算法,而且要求输出实例的大小和参数都是输入实例参数的函数。本文中,我们通过核化技术研究一些一阶逻辑子逻辑(通过限定一阶逻辑的布尔连接词和量词得到的逻辑)的模型检测问题的参数复杂性。
本文中引用了最近提出的蒸馏机制。首先我们证明了正存在式一阶逻辑在二分图上的参数模型检测问题存在线性核,其中参数为输入语句的长度。其次,在相同的参数情况下,我们证明了存在式一阶逻辑在路径上的参数模型检测问题有线性核。最后,在的假设下,对于固定的结构,我们证明了存在式或全称式一阶逻辑的参数模型检测问题没有多项式核,此时的参数为语句中的变元个数。
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.
本文中引用了最近提出的蒸馏机制。首先我们证明了正存在式一阶逻辑在二分图上的参数模型检测问题存在线性核,其中参数为输入语句的长度。其次,在相同的参数情况下,我们证明了存在式一阶逻辑在路径上的参数模型检测问题有线性核。最后,在的假设下,对于固定的结构,我们证明了存在式或全称式一阶逻辑的参数模型检测问题没有多项式核,此时的参数为语句中的变元个数。
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.
引文
[1]H. L. Bodlaender, R. G. Downey, M. R. Fellows and D. Hermelin. On problems without polynomial kernels. To appear in Proceedings of the 35th International Colloquium on Automata, Languages and Programming (ICALP'08, Track A),2008.
[2]H. Buhrman and J. M. Hitchcock. NP-hard sets are exponentially dense unless coNP C NP/poly. In Proceedings of the 23rd Annual IEEE Conference on Computational Complexity (CCC'08), pp.1-7, 2008. Electronic Colloquium on Computational Complexity (ECCC'08), Report TR08-022, available at http://eccc.hpi-web.de/eccc-local/Lists/TR-2008.html
[3]V. Arvind, J. Kobler and M. Mundhenk. On bounded truth-table, conjunctive, and randomized reductions to sparse sets. In Proceedings of the 12th Conference on the Foundations of Software Technology and Theoreti-cal Computer Science,pp.140-151, Vol.652,1992.
[4]O. Lichtenstein and A. Pnueli. Finite state concurrent programs satisfy their linear specification. InProceedings of the Twelfth ACM Symposium on the Principles of Programming Languages,pp.97-107, 1985.
[5]L.J. Stockmeyer. The Complexity of Decision Problems in Automata Theory. Ph.D. Thesis, Department of Electrical Engineering, MIT,1974.
[6]M.Y. Vardi. The complexity of relational query languages. In Proceedings of the 14th ACM Symposium on Theory of Computing, pp.137-146,1982.
[7]D. Seese. Linear time computable problems and first-order descriptions. Mathematical Structures in Com-puter Science, Vol.6, pp.505-626,1996.
[8]J. Flum and M. Grohe. Fixed-parameter tractability, definability, and model checking. SIAM Journal on Computing 31, page 113-145,2001.
[9]I. Dinur. The PCP theorem by gap amplification. Electronic Colloquium on Computational Complexity (ECCC'05), Report TR05-046 2005.
[10]Y. Chen, J. Flum and M. Muller. Lower bounds for kernelizations. Electronic Colloquium on Computational Complexity (ECCC'07), Report TR07-137 2007.
[11]R.G. Downey and M.R. Fellows. Parameterized Complexity, Springer,1999.
[12]J. Flum and M. Grohe. Parameterized Complexity Theory, Springer,2006.
[13]P. Hell and J. Nesetriland. On the complexity of H-coloring. J. Comb. Theory, Ser. B 48(1), page 92-110, 1990.
[14]L. Fortnow and R. Santhanam. Infeasibility of instance compression and succinct PCPs for NP Electronic Colloquium on Computational Complexity (ECCC'07), Report TR07-096,2007, available at http://eccc.hpi-web. de/eccc-local/Lists/TR-2007.html. Revised version available at http://lance.fortnow.com/papers/
[15]J. Guo and R. Niedermeier. Invitation to data reduction and problem kernelization. ACM SIGACT News, Vol. 38, No.1,2007.
[16]D. Harnik and M. Naor. On the compressibility of NP instances and cryptographic applications, In Proceed-ings of the 47th Annual IEEE Symposium on Foundations of Computer Science (FOCS'06), pp.719-728, 2006. Full version appears as Electronic Colloquium on Computational Complexity, Report TR06-022,2006, available at http://eccc.hpi-web. de/eccc-local/Lists/TR-2006.html
[17]S. Mahaney. Sparse complete sets for NP:solution of a conjecture of Berman and Hartmanis. Journal of Computer and System Sciences, Vol.25, pp.130-143,1982.
[18]J. Naor and M. Naor. Small-bias probability spaces:efficient constructions and applications SIAM Journal on Computing, Vol.22, No.22, pp.213-223,1993.
[19]R. Niedermeier. Invitation to Fixed-Parameter Algorithms, Oxford University Press,2006.
[20]D. Ranjan and P. Rohatgi. On randomized reductions to sparse sets, Proceedings of the 7th Annual Structure in Complexity Theory Conference,1992.
[21]C. K. Yap. Some consequences of non-uniform conditions on uniform classes, Theoretical Computer Science 26, page 287-300,1983.
[22]L. Cai, J. Chen, R. Downey and M. Fellows. Advice classes of parameterized tractablity, Annals of Pure and Applied logic 84, page 119-138,1997.
[23]Barnaby Martin. First-Order Model Checking Problems Parameterized by the Model, Conference on Com-putability in Europe, page 417-427,2008.
[24]G. J. Myers. The art of software testings, Wiley,1979.
[25]Michael Huth and M. Ryan. Logic in Computer Science:Modelling and Reasoning about Systems. CMU, 1999.
[26]Edmund M. Clarke, Orna Grumberg and Doron A. Peled. Model Checking. MIT Press,1999.
[27]H. R. Lewis and C. H. Papadimitriou. Elements of the theory of computation. Prentice Hall,1997.
[28]Xuan Cai. Linear Kernelizations for Restricted 3-Hitting Set Problems. Information Processing Letters., 2009.
[29]J. Chen, H. Fernau, IA. Kanj and G. Xia. Parametric duality and kernelization:Lower bounds and upper bounds on kernel size SIAM Journal on Computing, vol.37, no.4,2007.
[30]M. Frick and M. Grohe. The complexity of first-order and monadic second-order logic revisited, Annals of Pure and Applied logic 130, page 3-31,2004.
[31]R.G. Downey, M.R. Fellows and U. Taylor. The parameterized complexity of relational database queries and an improved characterization of W[1], In Bridges, Calude, Gibbons, Reeves, andWitten, editors, Combina-torics, Complexity, and Logic-Proceedings of DMTCS'96, pages 194-213. Springer-Verlag,1996.
[32]A.K. Chandra and P.M. Merlin. Optimal implementation of conjunctive queries in relational data bases, Proceedings of the 9th ACM Symposium on Theory of Computing, pages 77-90,1977.
[33]C.H. Papadimitriou and M. Yannakakis. On the complexity of database queries, Proceedings of the 17th ACM Symposium on Principles of Database Systems, pages 12-19,1997.
[34]Ch. Chekuri and A. Rajaraman. Conjunctive query containment revisited, Proceedings of the 5th Interna-tional Conference on Database Theory, volume 1186 of Lecture Notes in Computer Science, pages 56-70. Springer-Verlag,1997.
[35]M. Grohe, T. Schwentick and L. Segoufm. When is the evaluation of conjunctive queries tractable, Sympo-sium on Theory of Computing, page 657-666,2001.
[36]H. Gaifman. On local and non-local properties, Proceedings of the Herbrand Symposium, Logic Colloquium 81, North Holland,1982.
[37]B. Courcelle. Graph rewriting:an algebraic and logic approach. In J. van Leeuwen (Ed.), Handbook of Theoretical Computer Science, vol. B, Elsevier Science Publishers, pp.194-242,1990.
[38]M. Frick and M. Grohe. Deciding first-order properties of locally tree-decomposable structures. Journal of the ACM, Vol.48, pp.1184-1206,2001.
[39]Anuj Dawar, Martin Grohe and Stephan Kreutzer. Locally Excluding a Minor, Proceedings of the 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), page 270-279,2007.
[40]M. Grohe. Gerneralize model-checking problems for first-order logic, Symposium on Theoretical Aspects of Computer Science (STACS'01), page 12-26,2001.
[2]H. Buhrman and J. M. Hitchcock. NP-hard sets are exponentially dense unless coNP C NP/poly. In Proceedings of the 23rd Annual IEEE Conference on Computational Complexity (CCC'08), pp.1-7, 2008. Electronic Colloquium on Computational Complexity (ECCC'08), Report TR08-022, available at http://eccc.hpi-web.de/eccc-local/Lists/TR-2008.html
[3]V. Arvind, J. Kobler and M. Mundhenk. On bounded truth-table, conjunctive, and randomized reductions to sparse sets. In Proceedings of the 12th Conference on the Foundations of Software Technology and Theoreti-cal Computer Science,pp.140-151, Vol.652,1992.
[4]O. Lichtenstein and A. Pnueli. Finite state concurrent programs satisfy their linear specification. InProceedings of the Twelfth ACM Symposium on the Principles of Programming Languages,pp.97-107, 1985.
[5]L.J. Stockmeyer. The Complexity of Decision Problems in Automata Theory. Ph.D. Thesis, Department of Electrical Engineering, MIT,1974.
[6]M.Y. Vardi. The complexity of relational query languages. In Proceedings of the 14th ACM Symposium on Theory of Computing, pp.137-146,1982.
[7]D. Seese. Linear time computable problems and first-order descriptions. Mathematical Structures in Com-puter Science, Vol.6, pp.505-626,1996.
[8]J. Flum and M. Grohe. Fixed-parameter tractability, definability, and model checking. SIAM Journal on Computing 31, page 113-145,2001.
[9]I. Dinur. The PCP theorem by gap amplification. Electronic Colloquium on Computational Complexity (ECCC'05), Report TR05-046 2005.
[10]Y. Chen, J. Flum and M. Muller. Lower bounds for kernelizations. Electronic Colloquium on Computational Complexity (ECCC'07), Report TR07-137 2007.
[11]R.G. Downey and M.R. Fellows. Parameterized Complexity, Springer,1999.
[12]J. Flum and M. Grohe. Parameterized Complexity Theory, Springer,2006.
[13]P. Hell and J. Nesetriland. On the complexity of H-coloring. J. Comb. Theory, Ser. B 48(1), page 92-110, 1990.
[14]L. Fortnow and R. Santhanam. Infeasibility of instance compression and succinct PCPs for NP Electronic Colloquium on Computational Complexity (ECCC'07), Report TR07-096,2007, available at http://eccc.hpi-web. de/eccc-local/Lists/TR-2007.html. Revised version available at http://lance.fortnow.com/papers/
[15]J. Guo and R. Niedermeier. Invitation to data reduction and problem kernelization. ACM SIGACT News, Vol. 38, No.1,2007.
[16]D. Harnik and M. Naor. On the compressibility of NP instances and cryptographic applications, In Proceed-ings of the 47th Annual IEEE Symposium on Foundations of Computer Science (FOCS'06), pp.719-728, 2006. Full version appears as Electronic Colloquium on Computational Complexity, Report TR06-022,2006, available at http://eccc.hpi-web. de/eccc-local/Lists/TR-2006.html
[17]S. Mahaney. Sparse complete sets for NP:solution of a conjecture of Berman and Hartmanis. Journal of Computer and System Sciences, Vol.25, pp.130-143,1982.
[18]J. Naor and M. Naor. Small-bias probability spaces:efficient constructions and applications SIAM Journal on Computing, Vol.22, No.22, pp.213-223,1993.
[19]R. Niedermeier. Invitation to Fixed-Parameter Algorithms, Oxford University Press,2006.
[20]D. Ranjan and P. Rohatgi. On randomized reductions to sparse sets, Proceedings of the 7th Annual Structure in Complexity Theory Conference,1992.
[21]C. K. Yap. Some consequences of non-uniform conditions on uniform classes, Theoretical Computer Science 26, page 287-300,1983.
[22]L. Cai, J. Chen, R. Downey and M. Fellows. Advice classes of parameterized tractablity, Annals of Pure and Applied logic 84, page 119-138,1997.
[23]Barnaby Martin. First-Order Model Checking Problems Parameterized by the Model, Conference on Com-putability in Europe, page 417-427,2008.
[24]G. J. Myers. The art of software testings, Wiley,1979.
[25]Michael Huth and M. Ryan. Logic in Computer Science:Modelling and Reasoning about Systems. CMU, 1999.
[26]Edmund M. Clarke, Orna Grumberg and Doron A. Peled. Model Checking. MIT Press,1999.
[27]H. R. Lewis and C. H. Papadimitriou. Elements of the theory of computation. Prentice Hall,1997.
[28]Xuan Cai. Linear Kernelizations for Restricted 3-Hitting Set Problems. Information Processing Letters., 2009.
[29]J. Chen, H. Fernau, IA. Kanj and G. Xia. Parametric duality and kernelization:Lower bounds and upper bounds on kernel size SIAM Journal on Computing, vol.37, no.4,2007.
[30]M. Frick and M. Grohe. The complexity of first-order and monadic second-order logic revisited, Annals of Pure and Applied logic 130, page 3-31,2004.
[31]R.G. Downey, M.R. Fellows and U. Taylor. The parameterized complexity of relational database queries and an improved characterization of W[1], In Bridges, Calude, Gibbons, Reeves, andWitten, editors, Combina-torics, Complexity, and Logic-Proceedings of DMTCS'96, pages 194-213. Springer-Verlag,1996.
[32]A.K. Chandra and P.M. Merlin. Optimal implementation of conjunctive queries in relational data bases, Proceedings of the 9th ACM Symposium on Theory of Computing, pages 77-90,1977.
[33]C.H. Papadimitriou and M. Yannakakis. On the complexity of database queries, Proceedings of the 17th ACM Symposium on Principles of Database Systems, pages 12-19,1997.
[34]Ch. Chekuri and A. Rajaraman. Conjunctive query containment revisited, Proceedings of the 5th Interna-tional Conference on Database Theory, volume 1186 of Lecture Notes in Computer Science, pages 56-70. Springer-Verlag,1997.
[35]M. Grohe, T. Schwentick and L. Segoufm. When is the evaluation of conjunctive queries tractable, Sympo-sium on Theory of Computing, page 657-666,2001.
[36]H. Gaifman. On local and non-local properties, Proceedings of the Herbrand Symposium, Logic Colloquium 81, North Holland,1982.
[37]B. Courcelle. Graph rewriting:an algebraic and logic approach. In J. van Leeuwen (Ed.), Handbook of Theoretical Computer Science, vol. B, Elsevier Science Publishers, pp.194-242,1990.
[38]M. Frick and M. Grohe. Deciding first-order properties of locally tree-decomposable structures. Journal of the ACM, Vol.48, pp.1184-1206,2001.
[39]Anuj Dawar, Martin Grohe and Stephan Kreutzer. Locally Excluding a Minor, Proceedings of the 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), page 270-279,2007.
[40]M. Grohe. Gerneralize model-checking problems for first-order logic, Symposium on Theoretical Aspects of Computer Science (STACS'01), page 12-26,2001.