Anneke Huijsmans: Optimising parity game solvers using dynamic SCC maintenance

Event Details

Two optimizations for Zielonka’s recursive algorithm for solving parity games are investigated. The first optimization is partial re-decomposition, in which only the part of the graph containing vertices of SCCs which have 1 or more vertices removed will be re-decomposed. The second optimization is dynamic SCC maintenance, which builds an SCC tree for each SCC and then maintains those when vertices or edges are removed from the graph. An implementation in Java is made for 3 versions of Zielonka’s algorithm: the first version is Zielonka’s algorithm with Tarjan’s algorithm as described in literature. The second version is Zielonka’s algorithm with the use of partial re-decomposition. The third version is Zielonka’s algorithm with dynamic SCC maintenance. The 3 versions are tested on various games. The conclusion from the tests is that Zielonka’s algorithm with partial re-decomposition gives the best improvement.