Summary: Parameterized complexity theory has led to a wide range of algorithmic breakthroughs within the last few decades, but the practicability of these methods for real-world problems is still not well understood. We investigate the practicability of one of the fundamental approaches of this field: dynamic programming on tree decompositions. Indisputably, this is a key technique in parameterized algorithms and modern algorithm design. Despite the enormous impact of this approach in theory, it still has very little influence on practical implementations. The reasons for this phenomenon are manifold. One of them is the simple fact that such an implementation requires a long chain of non-trivial tasks (as computing the decomposition, preparing it, …). We provide an easy way to implement such dynamic programs that only requires the definition of the update rules. With this interface, dynamic programs for various problems, such as 3-coloring, can be implemented easily in about 100 lines of structured Java code. The theoretical foundation of the success of dynamic programming on tree decompositions is well understood due to Courcelle’s celebrated theorem, which states that every MSO-definable problem can be efficiently solved if a tree decomposition of small width is given. We seek to provide practical access to this theorem as well, by presenting a lightweight model checker for a small fragment of MSO$$_1$$ (that is, we do not consider “edge-set-based” problems). This fragment is powerful enough to describe many natural problems, and our model checker turns out to be very competitive against similar state-of-the-art tools.

### MSC:

 68Q27 Parameterized complexity, tractability and kernelization 68Q60 Specification and verification (program logics, model checking, etc.) 68R10 Graph theory (including graph drawing) in computer science 68W05 Nonnumerical algorithms 90C39 Dynamic programming

### Keywords:

fixed-parameter tractability; treewidth; model checking

D-FLAT; Jdrasil
Full Text:

### References:

 [1] Cygan, M.; Fomin, F.V.; Kowalik, Ł.; Lokshtanov, D.; Marx, D.; Pilipczuk, M.; Pilipczuk, M.; Saurabh, S.; ; Parameterized Algorithms: Berlin, Germany 2015; . [2] Dell, H.; Husfeldt, T.; Jansen, B.M.P.; Kaski, P.; Komusiewicz, C.; Rosamond, F.A.; The first parameterized algorithms and computational experiments challenge; Proceedings of the 11th International Symposium on Parameterized and Exact Computation (IPEC): ; ,30:1-30:9. [3] Dell, H.; Komusiewicz, C.; Talmon, N.; Weller, M.; The PACE 2017 parameterized algorithms and computational experiments challenge: The second iteration; Proceedings of the 12th International Symposium on Parameterized and Exact Computation (IPEC): ; ,30:1-30:12. [4] Courcelle, B.; The monadic second-order logic of graphs. I. Recognizable sets of finite graphs; Inf. Comput.: 1990; Volume 85 ,12-75. · Zbl 0722.03008 [5] Bodlaender, H.L.; A linear-time algorithm for finding tree-decompositions of small treewidth; SIAM J. Comput.: 1996; Volume 25 ,1305-1317. · Zbl 0864.68074 [6] Tamaki, H.; Positive-Instance driven dynamic programming for treewidth; Proceedings of the 25th Annual European Symposium on Algorithms (ESA): ; ,68:1-68:13. · Zbl 1426.90250 [7] Abseher, M.; Bliem, B.; Charwat, G.; Dusberger, F.; Hecher, M.; Woltran, S.; D-FLAT: Progress Report; ; . [8] Langer, A.J.; Fast Algorithms for Decomposable Graphs; Ph.D. Thesis: Aachen, Germany 2013; . [9] Diestel, R.; ; Graph Theory: Springer Graduate Text Gtm 173: Berlin, Germany 2012; Volume Volume 173 . [10] Flum, J.; Grohe, M.; ; Parameterized Complexity Theory: Berlin, Germany 2006; . [11] Bannach, M.; Berndt, S.; Ehlers, T.; Jdrasil: A modular library for computing tree decompositions; Proceedings of the 16th International Symposium on Experimental Algorithms (SEA): ; ,28:1-28:21. · Zbl 1433.68275 [12] Bannach, M.; Jdrasil for Graph Coloring; ; . · Zbl 1433.68275 [13] Bannach, M.; Berndt, S.; Ehlers, T.; Jdrasil; ; . · Zbl 1433.68275 [14] Frick, M.; Grohe, M.; The complexity of first-order and monadic second-order logic revisited; Ann. Pure Appl. Logic: 2004; Volume 130 ,3-31. · Zbl 1062.03032 [15] Kneis, J.; Langer, A.; Rossmanith, P.; Courcelle’s theorem—A game-theoretic approach; Discret. Optim.: 2011; Volume 8 ,568-594. · Zbl 1235.68103 [16] Bannach, M.; Berndt, S.; Jatatosk; ; . [17] Fichte, J.K.; gtfs2graphs—A Transit Feed to Graph Format Converter; ; . [18] Fichte, J.K.; Lodha, N.; Szeider, S.; SAT-Based local improvement for finding tree decompositions of small width; Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (SAT): Cham, Switzerland 2017; ,401-411. · Zbl 06807239 [19] Abseher, M.; Dusberger, F.; Musliu, N.; Woltran, S.; Improving the efficiency of dynamic programming on tree decompositions via machine learning; J. Artif. Intell. Res.: 2015; Volume 58 ,275-282.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.