Parity games and propositional proofs

ABSTRACT. Parity games are a class of two player games played by moving a token around a finite graph. They have important applications in automata theory, logic and verification. The main computational problem for such games is to decide which player has a winning strategy. This problem is reducible to a search problem in the intersection of the classes PLS and PPAD, but is not known to be in P, despite intensive research work.

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 resolution is weakly automatizable, then the decision problem for parity games is in P.

We also give simple proofs that the same holds for depth-1 propositional calculus (where resolution has depth 0) with respect to the related classes of mean payoff games and simple stochastic games, reproving results from [1, 3].

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 arithmetic theory proves that both players in a game cannot simultaneously have a winning strategy, and then to translate this proof into propositional form.

This work has been accepted for publication as [2].