In this work, we introduce TreeWidzard, an engine for developing dynamic programming algorithms that decide graph-theoretic properties parameterized by treewidth and pathwidth. Besides providing a unified framework for algorithms deciding atomic graph-theoretic properties, our engine allows one to combine such algorithms for two purposes: to obtain dynamic programming algorithms for more complex graph properties, and to support treewidth-based automated theorem proving. Within this context, given the specification of a Boolean combination \(P\) of graph properties \(P_1, P_2, \ldots, P_r\), and a positive integer \(k\), our engine can be used to determine whether all graphs of treewidth at most \(k\) satisfy \(P\). The main goal of the present work is to provide a system description of TreeWidzard. In particular, we provide a step-by-step account of how to implement dynamic programming algorithms in our framework and how to combine these algorithms for model checking and automated theorem proving.

翻译：摘要：本文介绍TreeWidzard——一种用于开发以树宽和路径宽为参数、判定图论性质的动态规划算法的引擎。该引擎不仅为判定原子图论性质的算法提供了统一框架，还允许用户为以下两个目的组合此类算法：一是获取更复杂图性质的动态规划算法，二是支持基于树宽的自动定理证明。在此框架下，给定图性质\(P_1, P_2, \ldots, P_r\)的布尔组合\(P\)的规范描述和正整数\(k\)，本引擎可用于判定所有树宽不超过\(k\)的图是否均满足性质\(P\)。本文的主要目标是对TreeWidzard进行系统描述，具体包括：提供在框架中实现动态规划算法的分步说明，以及如何组合这些算法以用于模型检测与自动定理证明。