Parity Games and Resolution

Arnold Beckmann Swansea University, Wales, UK   Homepage

Parity games are two player games which are played by moving a token around a finite graph. Parity games have important applications in automata theory, logic, and verification. It is a long-standing open problem whether the winner in a parity game can be decided in polynomial time. In the talk, we will relate this problem to weak automatizability of resolution using bounded arithmetic. 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. Namely, we will show that if the resolution proof system is weakly automatizable, then parity games can be decided in polynomial time.

This is joint work with Pavel Pudlak and Neil Thapen.