Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2605.09732 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911669912862720 |
|---|---|
| author | Oliveria, Mateus de Oliveira Urmian, Sam |
| author_facet | Oliveria, Mateus de Oliveira Urmian, Sam |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_09732 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | TreeWidzard: An Engine for Width-Based Dynamic Programming and Automated Theorem Proving Oliveria, Mateus de Oliveira Urmian, Sam Data Structures and Algorithms Logic in Computer Science Combinatorics 68R10, 68W40, 05C85, 68Q60, 03B70, 68Q27 F.2.2; G.2.2; F.4.1; I.2.3; G.4 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. |
| title | TreeWidzard: An Engine for Width-Based Dynamic Programming and Automated Theorem Proving |
| topic | Data Structures and Algorithms Logic in Computer Science Combinatorics 68R10, 68W40, 05C85, 68Q60, 03B70, 68Q27 F.2.2; G.2.2; F.4.1; I.2.3; G.4 |
| url | https://arxiv.org/abs/2605.09732 |