Talk

Solving Parity Games by a Reduction to SAT

Martin Lange

University of Munich

Abstract

This paper presents a reduction from the problem of solving parity games to the satisfiability problem for formulas of propositional logic in conjunctive normal form. It uses Jurdzinski's characterization of winning strategies via progress measures. The reduction is motivated by the apparent success that using SAT solvers has had in symbolic verification. The paper reports on a prototype implementation of the reduction and presents some runtime results.