Mean-payoff games and propositional proofs
| Autor: | Albert Atserias, Elitza Maneva |
|---|---|
| Přispěvatelé: | Centre de Recerca Matemàtica |
| Rok vydání: | 2011 |
| Předmět: |
Computer Science::Computer Science and Game Theory
Polynomial Computational complexity theory Demostració Teoria de la Automatizability Computer Science::Computational Complexity Mathematical proof 510 - Consideracions fonamentals i generals de les matemàtiques Theoretical Computer Science Mean-payoff games Feasible interpolation Integer Frege proof system Computer Science::Logic in Computer Science Time complexity Mathematics Discrete mathematics Proof complexity Resolution (logic) Computer Science Applications TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Computational Theory and Mathematics Resolution Information Systems Interpolation |
| Zdroj: | Recercat. Dipósit de la Recerca de Catalunya instname |
| ISSN: | 0890-5401 |
| DOI: | 10.1016/j.ic.2011.01.003 |
| Popis: | We 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 @S"2-Frege (i.e. DNF-resolution). This reduces mean-payoff games to the weak automatizability of @S"2-Frege, and to the interpolation problem for @S"2","2-Frege. Since the interpolation problem for @S"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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect