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

Preprint · Mateus de Oliveira Oliveria, Sam Urmian

- Archive id: arxiv:2605.09732
- Published: 2026-05-10
- arXiv: https://arxiv.org/abs/2605.09732
- Source URL: https://arxiv.org/abs/2605.09732
- PDF: https://arxiv.org/pdf/2605.09732
- Provenance: arxiv

## 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.

_Abstract reproduced under CC0-1.0 (arXiv descriptive metadata)._

---
Space Kitty Archive · https://space-kitty.com · API: https://space-kitty.com/api/v1 · MCP: https://space-kitty.com/mcp · Premium: $0.20/request via x402 (Base Sepolia (testnet)). Metadata: arXiv (CC0), OpenAlex (CC0), Europe PMC (CC BY/CC0 works), ClinicalTrials.gov.