Parity games and propositional proofs

A propositional proof system is weakly automatizable if there is a polynomial time algorithm which separates satisfiable formulas from formulas which have a short refutation in the system, with respect to a given length bound. We show that if the resolution proof system is weakly automatizable, then parity games can be decided in poly-nomial time. We give simple proofs that the same holds for depth-1 propositional calculus (where resolution has depth 0) with respect to mean payoff and simple stochastic games. We define a new type of combinatorial game and prove that resolution is weakly automatizable if and only if one can separate, by a set decidable in polynomial time, the games in which the first player has a positional winning strategy from the games in which the second player has a positional winning strategy. Our main technique is to show that a suitable weak bounded arith-metic theory proves that both players in a game cannot simultaneously have a winning strategy, and then to translate this proof into proposi-tional form. ∗This research was partially done while the authors were visiting fellows at the Isaac Newton Institute for the Mathematical Sciences in the programme “Semantics & Syntax”. †Partially supported by grant IAA100190902 of GA AV Č