NOC Propagators for Solving Parity Games - Appendix

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 of 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.