License: Creative Commons Attribution-NoDerivs 3.0 Unported license (CC BY-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.STACS.2010.2494
URN: urn:nbn:de:0030-drops-24940
Go to the corresponding LIPIcs Volume Portal

Williams, Ryan

Alternation-Trading Proofs, Linear Programming, and Lower Bounds

1001.WilliamsRyan.2494.pdf (0.3 MB)


A fertile area of recent research has demonstrated concrete polynomial time lower bounds for solving natural hard problems on restricted computational models. Among these problems are Satisfiability, Vertex Cover, Hamilton Path, $\text{MOD}_6\text{-SAT}$, Majority-of-Majority-SAT, and Tautologies, to name a few. The proofs of these lower bounds follow a certain proof-by-contradiction strategy that we call {\em alternation-trading}. An important open problem is to determine how powerful such proofs can possibly be.

We propose a methodology for studying these proofs that makes them amenable to both formal analysis and automated theorem proving. We prove that the search for better lower bounds can often be turned into a problem of solving a large series of linear programming instances. Implementing a small-scale theorem prover based on this result, we extract new human-readable time lower bounds for several problems. This framework can also be used to prove concrete limitations on the current techniques.

BibTeX - Entry

  author =	{Ryan Williams},
  title =	{{Alternation-Trading Proofs, Linear Programming, and Lower Bounds}},
  booktitle =	{27th International Symposium on Theoretical Aspects of Computer Science},
  pages =	{669--680},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-16-3},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{5},
  editor =	{Jean-Yves Marion and Thomas Schwentick},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{},
  URN =		{urn:nbn:de:0030-drops-24940},
  doi =		{10.4230/LIPIcs.STACS.2010.2494},
  annote =	{Keywords: Time-space tradeoffs, lower bounds, alternation, linear programming}

Keywords: Time-space tradeoffs, lower bounds, alternation, linear programming
Collection: 27th International Symposium on Theoretical Aspects of Computer Science
Issue Date: 2010
Date of publication: 09.03.2010

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI