When: Wednesday, June 15, 2pm
Where: room G2.91b
Abstract
Courcelle's Theorem states that all MSO-definable problems can be solved in linear time on graphs of bounded treewidth. The standard approach of constructing a tree automaton from the MSO-formula and running this automaton on the tree decomposition often fails because the automaton cannot be constructed. We implemented a program that does not use tree automata, but constructs game trees for each node of the tree decomposition. From these game trees optimal solutions can easily be computed. Several algorithmic improvements were necessary to turn this idea into practically useful software.
Joint work with Peter Rossmanith