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

TL;DR

TreeWidzard is a versatile engine that facilitates the development of dynamic programming algorithms for graph properties based on treewidth, enabling automated theorem proving and complex property analysis.

Contribution

The paper introduces TreeWidzard, a unified framework for creating dynamic programming algorithms for graph properties and supporting automated theorem proving based on treewidth.

Findings

Provides a systematic method to implement dynamic programming algorithms in TreeWidzard.

Enables combining algorithms for complex graph property analysis.

Supports automated theorem proving for graph properties.

Abstract

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.