ECCC-Report TR13-092https://eccc.weizmann.ac.il/report/2013/092Comments and Revisions published for TR13-092en-usFri, 21 Jun 2013 09:29:30 +0300
Revision 1
| Parity Games and Propositional Proofs |
Pavel Pudlak,
Neil Thapen,
Arnold Beckmann
https://eccc.weizmann.ac.il/report/2013/092#revision1A propositional proof system is \emph{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 polynomial 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 in
P, the games in which the first player has a positional 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.Fri, 21 Jun 2013 09:29:30 +0300https://eccc.weizmann.ac.il/report/2013/092#revision1
Paper TR13-092
| Parity Games and Propositional Proofs |
Pavel Pudlak,
Neil Thapen,
Arnold Beckmann
https://eccc.weizmann.ac.il/report/2013/092A propositional proof system is \emph{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 polynomial 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 in
P, the games in which the first player has a positional 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.Wed, 19 Jun 2013 10:31:00 +0300https://eccc.weizmann.ac.il/report/2013/092