TreeWidzard: An Engine for Width-Based Dynamic Programming and Automated Theorem Proving
This work provides a unified framework for researchers and practitioners to implement and combine treewidth-based dynamic programming algorithms for automated theorem proving.
TreeWidzard is an engine for dynamic programming algorithms parameterized by treewidth and pathwidth, enabling automated theorem proving for graph properties. It allows combining atomic algorithms to decide complex Boolean combinations of properties for graphs of bounded treewidth.
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.