Solving Parity Games by a Reduction to SAT

Reference:

Keijo Heljanko, Misa Keinänen, Martin Lange, and Ilkka Niemelä. Solving parity games by a reduction to SAT. Journal of Computer and System Sciences, 78(2):430–440, 2012.

Abstract:

This paper presents a reduction from the problem of solving parity games to the satisfiability problem in propositional logic (SAT). The reduction is done in two stages, first into difference logic, i.e. SAT combined with the theory of integer differences, an instance of the SAT modulo theories (SMT) framework. In the second stage the integer variables and constraints of the difference logic encoding are replaced with a set of Boolean variables and constraints on them, giving rise to a pure SAT encoding of the problem. The reduction uses Jurdzińskiʼs characterisation of winning strategies via progress measures. The reduction is motivated by the success of SAT solvers in symbolic verification, bounded model checking in particular. The paper reports on prototype implementations of the reductions and presents some experimental results.

Keywords:

Parity games, Propositional satisfiability, Difference logic

Suggested BibTeX entry:

@article{HelKeiLanNie:JCSS,
    author = {Keijo Heljanko and Misa Keinänen and Martin Lange and Ilkka Niemelä},
    journal = {Journal of Computer and System Sciences},
    language = {eng},
    number = {2},
    pages = {430-440},
    title = {Solving Parity Games by a Reduction to {SAT}},
    volume = {78},
    year = {2012},
}