No-Opponent-Cycle Propagators for Solving Parity Games
摘要
Solving parity games is a core problem in formal verification, specifically when using model checking and synthesis methods, which have several industrial-scale applications. In this paper, we propose a constraint-based approach for parity games, built upon a new propagation algorithm that eliminates opponent cycles from the game graph. This approach results in an efficient method that exploits the duality between the players in a parity game. Our implementation within a Lazy Clause Generation framework outperforms all existing constraint-based methods for parity games and performs competitively against the most specialized non-CP-based algorithms—often matching and sometimes exceeding their performance—while retaining the flexibility inherent to general constraint-based approaches. Since new constraints can be easily added, our method provides a flexible framework for refining existing problem formulations to search for preferred solutions by satisfying additional constraints. This feature can also be used to solve parity games where additional quantitative constraints (e.g., cost or resource-bounded requirements) need to be satisfied. We present the theoretical foundations of the approach, an experimental evaluation, and a discussion of the results, including an analysis of different versions of the new propagator.