Ryan Williams
ABSTRACT
First-order logic captures a vast number of computational problems on graphs. We study the time complexity of deciding graph properties definable by first-order sentences in prenex normal form with k variables. The trivial algorithm for this problem runs in O(nk) time on n-node graphs (the big-O hides the dependence on k).
Answering a question of Miklós Ajtai, we give the first algorithms running faster than the trivial algorithm, in the general case of arbitrary first-order sentences and arbitrary graphs. One algorithm runs in O(nk-3+ω) ≤ O(nk-0.627) time for all k ≥ 3, where ω < 2.373 is the n x n matrix multiplication exponent. By applying fast rectangular matrix multiplication, the algorithm can be improved further to run in nk-1+o(1) time, for all k ≥ 9. Finally, we observe that the exponent of k - 1 is optimal, under the popular hypothesis that CNF satisfiability with n variables and m clauses cannot be solved in (2 - ε)n · poly(m) time for some ε > 0.
- {AV14} Amir Abboud and Virginia Vassilevska Williams. Popular conjectures imply strong lower bounds for dynamic problems. arXiv:1402.0054, 2014.Google Scholar
- {AVW14} Amir Abboud, Virginia Vassilevska Williams, and Oren Weimann. Consequences of faster alignment of sequences. In ICALP, to appear, 2014.Google Scholar
- {CDL+12} Marek Cygan, Holger Dell, Daniel Lokshtanov, Dániel Marx, Jesper Nederlof, Yoshio Okamoto, Ramamohan Paturi, Saket Saurabh, and Magnus Wahlström. On problems as hard as CNF-SAT. In IEEE Conference on Computational Complexity, pages 74--84, 2012. Google ScholarDigital Library
- {CHKX06} Jianer Chen, Xiuzhen Huang, Iyad A. Kanj, and Ge Xia. Strong computational lower bounds via parameterized complexity. J. Comput. Syst. Sci., 72(8):1346--1367, 2006. Google ScholarDigital Library
- {CIP09} Chris Calabro, Russell Impagliazzo, and Ramamohan Paturi. The complexity of satisfiability of small depth circuits. In Parameterized and Exact Computation, pages 75--85. Springer, 2009. Google ScholarDigital Library
- {CKN13} Marek Cygan, Stefan Kratsch, and Jesper Nederlof. Fast Hamiltonicity checking via bases of perfect matchings. In STOC, pages 301--310, 2013. Google ScholarDigital Library
- {CNP+11} Marek Cygan, Jesper Nederlof, Marcin Pilipczuk, J. M. M. van Rooij, and J. O. Wojtaszczyk. Solving connectivity problems parameterized by treewidth in single exponential time. In FOCS, pages 150--159, 2011. Google ScholarDigital Library
- {Cop97} Don Coppersmith. Rectangular matrix multiplication revisited. Journal of Complexity, 13:42--49, 1997. Google ScholarDigital Library
- {Cou90} Bruno Courcelle. The monadic second-order logic of graphs. i. recognizable sets of finite graphs. Information and Computation, 85(1):12--75, 1990. Google ScholarDigital Library
- {Cyg12} Marek Cygan. Deterministic parameterized connected vertex cover. In Algorithm Theory--SWAT 2012, pages 95--106. Springer, 2012. Google ScholarDigital Library
- {DF99} Rodney G. Downey and Michael R. Fellows. Springer-Verlag, 1999.Google Scholar
- {DKT10} Zdenek Dvorak, Daniel Král, and Robin Thomas. Deciding first-order properties for sparse graphs. In FOCS, pages 133--142, 2010. Google ScholarDigital Library
- {DW10} Evgeny Dantsin and Alexander Wolpert. On moderately exponential time for SAT. In Proc. 13th International Conference on Theory and Applications of Satisfiability Testing, pages 313--325, 2010. Google ScholarDigital Library
- {EG04} Friedrich Eisenbrand and Fabrizio Grandoni. On the complexity of fixed parameter clique and dominating set. Theor. Comput. Sci., 326(1-3):57--67, 2004. Google ScholarDigital Library
- {FG04} Markus Frick and Martin Grohe. The complexity of first-order and monadic second-order logic revisited. Ann. Pure Appl. Logic, 130(1-3):3--31, 2004.Google ScholarCross Ref
- {FG06} Jörg Flum and Martin Grohe. Parameterized complexity theory, volume 3. Springer Heidelberg, 2006.Google Scholar
- {FHV13} Henning Fernau, Pinar Heggernes, and Yngve Villanger. A multivariate analysis of some DFA problems. In Proceedings of LATA, pages 275--286, 2013.Google ScholarCross Ref
- {Gal12} François Le Gall. Faster algorithms for rectangular matrix multiplication. In FOCS, pages 514--523, 2012. Google ScholarDigital Library
- {HKN12} Sepp Hartung, Christian Komusiewicz, and André Nichterlein. Parameterized algorithmics and computational experiments for finding 2-clubs. In Parameterized and Exact Computation, pages 231--241. Springer, 2012. Google ScholarDigital Library
- {HP98} Xiaohan Huang and Victor Y. Pan. Fast rectangular matrix multiplication and applications. J. Complexity, 14(2):257--299, 1998. Google ScholarDigital Library
- {IP01} Russell Impagliazzo and Ramamohan Paturi. On the complexity of k-SAT. J. Comput. Syst. Sci., 62(2):367--375, 2001. Google ScholarDigital Library
- {IPZ01} Russell Impagliazzo, Ramamohan Paturi, and Francis Zane. Which problems have strongly exponential complexity? J. Comput. Syst. Sci., 63(4):512--530, 2001. Google ScholarDigital Library
- {LMS11} Daniel Lokshtanov, Dániel Marx, and Saket Saurabh. Known algorithms on graphs on bounded treewidth are probably optimal. In SODA, pages 777--789, 2011. Google ScholarDigital Library
- {NP85} Jaroslav Nešetřil and Svatopluk Poljak. On the complexity of the subgraph problem. Commentationes Mathematicae Universitatis Carolinae, 26(2):415--419, 1985.Google Scholar
- {PP12} Marcin Pilipczuk and Michał Pilipczuk. Finding a maximum induced degenerate subgraph faster than 2n. In Parameterized and Exact Computation, pages 3--12. Springer, 2012. Google ScholarDigital Library
- {PW10} Mihai Patraşcu and Ryan Williams. On the possibility of faster sat algorithms. In SODA, pages 1065--1075, 2010. Google ScholarDigital Library
- {RV13} Liam Roditty and Virginia Vassilevska Williams. Fast approximation algorithms for the diameter and radius of sparse graphs. In STOC, pages 515--524, 2013. Google ScholarDigital Library
- {Sto74} Larry J. Stockmeyer. The Complexity of Decision Problems in Automata Theory. PhD thesis, MIT, 1974.Google Scholar
- {Var82} Moshe Y. Vardi. The complexity of relational query languages. In STOC, pages 137--146, 1982. Google ScholarDigital Library
- {Vas12} Virginia Vassilevska Williams. Multiplying matrices faster than Coppersmith-Winograd. In STOC, pages 887--898, 2012. Google ScholarDigital Library
- {WY14} Ryan Williams and Huacheng Yu. Finding orthogonal vectors in discrete structures. In SODA, pages 1867--1877, 2014. Google ScholarDigital Library
Index Terms
- Faster decision of first-order graph properties
Recommendations
Formalization of the Resolution Calculus for First-Order Logic
I present a formalization in Isabelle/HOL of the resolution calculus for first-order logic with formal soundness and completeness proofs. To prove the calculus sound, I use the substitution lemma, and to prove it complete, I use Herbrand interpretations ...
On the complexity of entailment in existential conjunctive first-order logic with atomic negation
We consider the entailment problem in the fragment of first-order logic (FOL) composed of existentially closed conjunctions of literals (without functions), denoted by FOL(@__ __,@__ __,@__ __"a). This problem can be recast as several fundamental ...
Where First-Order and Monadic Second-Order Logic Coincide
We study on which classes of graphs first-order logic (fo) and monadic second-order logic (mso) have the same expressive power. We show that for all classes C of graphs that are closed under taking subgraphs, fo and mso have the same expressive power on ...
Comments