ECCC-Report TR10-197https://eccc.weizmann.ac.il/report/2010/197Comments and Revisions published for TR10-197en-usTue, 14 Dec 2010 11:06:37 +0200
Paper TR10-197
| Mean-payoff games and propositional proofs |
Albert Atserias,
Elitza Maneva
https://eccc.weizmann.ac.il/report/2010/197We associate a CNF-formula to every instance of the mean-payoff game problem in such a way that if the value of the game is non-negative the formula is satisfiable, and if the value of the game is negative the formula has a polynomial-size refutation in $\Sigma_2$-Frege (i.e.~DNF-resolution). This reduces mean-payoff games to the weak automatizability of $\Sigma_2$-Frege, and to the interpolation problem for $\Sigma_{2,2}$-Frege. Since the interpolation problem for $\Sigma_1$-Frege (i.e.~resolution) is solvable in polynomial time, our result is close to optimal up to the computational complexity of solving mean-payoff games. The proof of the main result requires building low-depth formulas that compute the bits of the sum of a constant number of integers in binary notation, and low-complexity proofs of the required arithmetic properties.
Tue, 14 Dec 2010 11:06:37 +0200https://eccc.weizmann.ac.il/report/2010/197