Parameterized Complexity of Fixed Variable Logics
We study the complexity of model checking formulas in first-order logic parameterized by the number of distinct variables in the formula. This problem, which is not known to be fixed-parameter tractable, resisted to be properly classified in the context of parameterized complexity. We show that it is complete for a newly-defined complexity class that we propose as an analog of the classical class PSPACE in parameterized complexity. We support this intuition by the following findings: First, the proposed class admits a definition in terms of alternating Turing machines in a similar way as PSPACE can be defined in terms of polynomial-time alternating machines. Second, we show that parameterized versions of other PSPACE-complete problems, like winning certain pebble games and finding restricted resolution refutations, are complete for this class.
Parameterized complexity
polynomial space
first-order logic
pebble games
regular resolutions
109-120
Regular Paper
Christoph
Berkholz
Christoph Berkholz
Michael
Elberfeld
Michael Elberfeld
10.4230/LIPIcs.FSTTCS.2014.109
Karl A. Abrahamson, Rodney G. Downey, and Michael R. Fellows. Fixed-parameter tractability and completeness IV: On completeness for \mathchoice W[P] W[P] W[P] W[P] and \mathchoice PSPACE PSPACE PSPACE PSPACE analogues. Annals of Pure and Applied Logic, 73(3):235-276, 1995.
Akeo Adachi, Shigeki Iwata, and Takumi Kasai. Some combinatorial game problems require Ω(n^k) time. J. ACM, 31:361-376, March 1984.
Christoph Berkholz. On the complexity of finding narrow proofs. In Foundations of Computer Science, IEEE Annual Symposium on, pages 351-360, Los Alamitos, CA, USA, 2012. IEEE Computer Society.
Christoph Berkholz. Lower bounds for existential pebble games and k-consistency tests. Logical Methods in Computer Science, 9(4), 2013.
Ashok K. Chandra, Dexter C. Kozen, and Larry J. Stockmeyer. Alternation. J. ACM, 28(1):114-133, 1981.
Yijia Chen, Jörg Flum, and Martin Grohe. Machine-based methods in parameterized complexity theory. Theoretical Computer Science, 339(2-3):167-199, 2005.
R. Downey and M. Fellows. Fixed-parameter tractability and completeness I: Basic results. SIAM Journal on Computing, 24(4):873-921, 1995.
Rodney G. Downey and Michael R. Fellows. Fundamentals of Parameterized Complexity. Texts in Computer Science. Springer, 2013.
Rodney G. Downey, Michael R. Fellows, and Ken Regan. Descriptive complexity and the \mathchoice W W W W-hierachy. In Proof Complexity and Feasible Arithmetic, volume 39 of AMS-DIMACS, pages 119-134. AMS, 1998.
Jörg Flum and Martin Grohe. Fixed-parameter tractability, definability, and model-checking. SIAM J. Comp., 31(1):113-145, 2001.
Jörg Flum and Martin Grohe. Model-checking problems as a basis for parameterized intractability. Logical Methods in Computer Science, 1(1), 2005.
Jörg Flum and Martin Grohe. Parameterized Complexity Theory. Springer, 2006.
Neil Immerman. Descriptive complexity. Springer, New York, 1999.
Takumi Kasai, Akeo Adachi, and Shigeki Iwata. Classes of pebble games and complete problems. SIAM J. Comput., 8(4):574-586, 1979.
Richard E Ladner. The circuit value problem is log space complete for \mathchoice P P P P. SIGACT News, 7:18-20, 1975.
Christos H. Papadimitriou and Mihalis Yannakakis. On the complexity of database queries. Journal of Computer and System Sciences, 58(3):407-427, 1999.
Larry J. Stockmeyer. The polynomial-time hierarchy. Theoretical Computer Science, 3(1):1-22, 1976.
Moshe Y. Vardi. The complexity of relational query languages (extended abstract). In Proceedings of the 15th Annual ACM Symposium on Theory of Computing (STOC 1982), pages 137-146. ACM, 1982.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode