TreeWidzard: An Engine for Width-Based Dynamic Programming and Automated Theorem Proving

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.