Partial Solvers for Parity Games: Effective Polynomial-Time Composition

TL;DR

This paper explores the composition of polynomial-time partial solvers for parity games, leading to new solvers that effectively solve standard benchmarks and almost all random game instances.

Contribution

It introduces generic composition patterns for partial solvers, resulting in new, more powerful solvers capable of solving complex parity games efficiently.

Findings

New partial solvers discovered through composition patterns

Solvers solve all standard benchmark games

One solver solves nearly all random game instances

Abstract

Partial methods play an important role in formal methods and beyond. Recently such methods were developed for parity games, where polynomial-time partial solvers decide the winners of a subset of nodes. We investigate here how effective polynomial-time partial solvers can be by studying interactions of partial solvers based on generic composition patterns that preserve polynomial-time computability. We show that use of such composition patterns discovers new partial solvers - including those that merge node sets that have the same but unknown winner - by studying games that composed partial solvers can neither solve nor simplify. We experimentally validate that this data-driven approach to refinement leads to polynomial-time partial solvers that can solve all standard benchmarks of structured games. For one of these polynomial-time partial solvers not even a sole random game from a few billion random games of varying configuration was found that it won't solve completely.