Abstract
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 Σ2-Frege (a.k.a. DNF-resolution). This reduces the problem of solving mean-payoff games to the weak automatizability of Σ2-Frege, and to the interpolation problem for Σ2,2-Frege. Since the interpolation problem for Σ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 their relevant arithmetic properties.
First author supported by CICYT TIN2007-68005-C04-03 (LOGFAC-2). Second author supported in part by MICINN Ramon y Cajal and CICYT TIN2007-66523 (FORMALISM). This work was done while visiting CRM, Bellaterra, Barcelona.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alekhnovich, M., Razborov, A.A.: Resolution is not automatizable unless W[P] is tractable. In: 42nd IEEE Symp. Found. of Comp. Sci., pp. 210–219 (2001)
Atserias, A., Bonet, M.L.: On the automatizability of resolution and related propositional proof systems. Information and Computation 189(2), 182–201 (2004)
Atserias, A., Bonet, M.L., Esteban, J.L.: Lower bounds for the weak pigeonhole principle and random formulas beyond resolution. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 136–152. Springer, Heidelberg (2001)
Atserias, A., Maneva, E.: Mean payoff-games and the max-atom problem. Technical report (2009), http://www.lsi.upc.edu/~atserias
Beame, P., Pitassi, T.: Simplified and improved resolution lower bounds. In: 37th IEEE Symp. Found of Comp. Sci., pp. 274–282 (1996)
Ben-Sasson, E., Wigderson, A.: Short proofs are narrow–resolution made simple. J. ACM 48(2), 149–169 (2001); Prelim. version in STOC 1999
Bezem, M., Nieuwenhuis, R., Rodríguez-Carbonell, E.: The max-atom problem and its relevance. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 47–61. Springer, Heidelberg (2008)
Björklund, H., Vorobyov, S.: Combinatorial structure and randomized subexponential algorithms for infinite games. Theor. Comp. Sci. 349(3), 347–360 (2005)
Bonet, M., Pitassi, T., Raz, R.: Lower bounds for cutting planes proofs with small coefficients. J. Symb. Logic 62(3), 708–728 (1997); Prelim. version in STOC 1995
Bonet, M.L., Domingo, C., Gavaldà, R., Maciel, A., Pitassi, T.: Non-automatizability of bounded-depth Frege proofs. Computational Complexity 13, 47–68 (2004); Prelim. version in CCC 1999
Bonet, M.L., Pitassi, T., Raz, R.: On interpolation and automatization for Frege systems. SIAM J. Comp. 29(6), 1939–1967 (2000); Prelim. version in FOCS 1997
Ehrenfeucht, A., Mycielsky, J.: Positional strategies for mean payoff games. International Journal of Game Theory 8(2), 109–113 (1979)
Furst, M., Saxe, J., Sipser, M.: Parity, circuits and the polynomial time hierarchy. Mathematical Systems Theory 17, 13–27 (1984)
Jurdziński, M.: Deciding the winner in parity games is in UP ∩ co-UP. Information Processing Letters 68, 119–124 (1998)
Jurdziński, M., Paterson, M., Zwick, U.: A deterministic subexponential algorithm for solving parity games. SIAM J. Comp. 38(4), 1519–1532 (2008)
Karp, R.M.: A characterization of the minimum cycle mean in a digraph. Discrete Mathematics 23(3), 309–311 (1978)
Krajícek, J.: Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. J. Symb. Logic 62, 457–486 (1997)
Krajícek, J., Pudlák, P.: Some consequences of cryptographical conjectures for \(S^1_2\) and EF. Information and Computation 140(1), 82–94 (1998)
Lovász, L., Plummer, M.D.: Matching Theory. AMS Chelsea Publ. (2009)
Möhring, R.H., Skutella, M., Stork, F.: Scheduling with AND/OR Precedence Constraints. SIAM J. Comp. 33(2), 393–415 (2004)
Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Reading (1995)
Pitassi, T., Santhanam, R.: Effectively polynomial simulations. In: Proceedings of First Symposium on Innovations in Computer Science, ICS (2010)
Pudlák, P.: Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symb. Logic 62(3), 981–998 (1997)
Pudlák, P.: On the complexity of the propositional calculus. In: Sets and Proofs, Invited Papers from Logic Colloq. 1997, pp. 197–218. Cambridge Univ. Press, Cambridge (1999)
Pudlák, P.: On reducibility and symmetry of disjoint NP-pairs. Theor. Comp. Sci. 295, 323–339 (2003)
Pudlák, P., Sgall, J.: Algebraic models of computation and interpolation for algebraic proof systems. In: Proof Complexity and Feasible Arithmetic. AMS (1998)
Zwick, U., Paterson, M.: The complexity of mean payoff games on graphs. Theor. Comp. Sci. 158, 343–359 (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Atserias, A., Maneva, E. (2010). Mean-Payoff Games and Propositional Proofs. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds) Automata, Languages and Programming. ICALP 2010. Lecture Notes in Computer Science, vol 6198. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14165-2_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-14165-2_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14164-5
Online ISBN: 978-3-642-14165-2
eBook Packages: Computer ScienceComputer Science (R0)