ALTERNATION-TRADING PROOFS, LINEAR PROGRAMMING, AND L OWER BOUNDS (EXTENDED ABSTRACT)

摘要: A fertile area of recent research has demonstrated concrete polynomial time lower bounds for solving natural hard problems on restricted computational models. Among these are Satisfiability, Vertex Cover, Hamilton Path, MOD6-SAT, Majority-of- Majority-SAT, and Tautologies, to name a few. The proofs follow certain proof-by-contradiction strategy that we call alternation-trading. An important open problem is determine how powerful such can possibly be. We propose methodology studying makes them amenable both formal analysis automated theorem proving. prove the search better often be turned into large series linear programming instances. Implementing small-scale prover based this result, extract new human-readable several problems. This framework also used limitations current techniques.