交替交易证明、线性规划和下限
Alternation-Trading Proofs, Linear Programming, and Lower Bounds
摘要：
最近的一个研究领域已经证明了在有限的计算模型上求解自然困难问题的具体多项式时间下界。这些问题包括可满足性、顶点覆盖、Hamilton路径、Mod 6-SAT、多数SAT和重言式等。这些下限的证明遵循一定的矛盾证明策略，我们称之为交替交易。一个重要的开放问题是确定这样的证明可能有多强大。我们提出了一种方法来研究这些证明，使他们能够进行正式分析和自动定理证明。我们证明，寻找更好的下界往往可以变成一个问题，解决了一系列的线性规划实例。实现一个小规模的定理证明的基础上，这个结果，我们提取新的人类可读的时间下限的几个问题。这个框架也可以用来证明目前技术的具体限制。
英文摘要：
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, Mod6-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 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
