# From Width-Based Model Checking to Width-Based Automated Theorem Proving

arXiv: https://arxiv.org/abs/2205.10995 · HTML: https://mlsanity.com/paper/2205.10995/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 18 of its 110 references that are in the map.
- First posted on arXiv 23 May 2022.

## Builds on (most cited first, 18 of 18)

- [Diversity of Solutions: An Exploration Through the Lens of Fixed-Parameter Tractability Theory](https://mlsanity.com/paper/1903.07410/) (2019)
- [A Single-Exponential Time 2-Approximation Algorithm for Treewidth](https://mlsanity.com/paper/2104.07463/) (2021)
- [Practical Access to Dynamic Programming on Tree Decompositions](https://mlsanity.com/paper/1806.10176/) (2018)
- [Finding Hamiltonian Cycle in Graphs of Bounded Treewidth: Experimental Evaluation](https://mlsanity.com/paper/1803.00927/) (2018)
- [Subgraphs Satisfying MSO Properties on z-Topologically Orderable Digraphs](https://mlsanity.com/paper/1303.4443/) (2013)
- [Computations by fly-automata beyond monadic second-order logic](https://mlsanity.com/paper/1305.7120/) (2013)
- [On triangulating k-outerplanar graphs](https://mlsanity.com/paper/1310.1845/) (2013)
- [Irrelevant Vertices for the Planar Disjoint Paths Problem](https://mlsanity.com/paper/1310.2378/) (2013)
- [Improved Bounds for the Flat Wall Theorem](https://mlsanity.com/paper/1410.0276/) (2014)
- [An Algorithmic Metatheorem for Directed Treewidth](https://mlsanity.com/paper/1410.0589/) (2014)
- [An FPT 2-Approximation for Tree-Cut Decomposition](https://mlsanity.com/paper/1509.04880/) (2015)
- [Definability equals recognizability for graphs of bounded treewidth](https://mlsanity.com/paper/1605.03045/) (2016)
- [Packing Cycles Faster Than ErdHos-P'osa](https://mlsanity.com/paper/1707.01037/) (2017)
- [Positive-Instance Driven Dynamic Programming for Graph Searching](https://mlsanity.com/paper/1905.01134/) (2019)
- [Hitting minors on bounded treewidth graphs. IV. An optimal algorithm](https://mlsanity.com/paper/1907.04442/) (2019)
- [A more accurate view of the Flat Wall Theorem](https://mlsanity.com/paper/2102.06463/) (2021)
- [On the Width of Regular Classes of Finite Structures](https://mlsanity.com/paper/2104.10286/) (2021)
- [Isolation schemes for problems on decomposable graphs](https://mlsanity.com/paper/2105.01465/) (2021)

## Abstract (arXiv)

In the field of parameterized complexity theory, the study of graph width measures has been intimately connected with the development of width-based model checking algorithms for combinatorial properties on graphs. In this work, we introduce a general framework to convert a large class of width-based model-checking algorithms into algorithms that can be used to test the validity of graph-theoretic conjectures on classes of graphs of bounded width. Our framework is modular and can be applied with respect to several well-studied width measures for graphs, including treewidth and cliquewidth. As a quantitative application of our framework, we prove analytically that for several long-standing graph-theoretic conjectures, there exists an algorithm that takes a number k as input and correctly determines in time double-exponential in kO(1) whether the conjecture is valid on all graphs of treewidth at most k. These upper bounds, which may be regarded as upper-bounds on the size of proofs/disproofs for these conjectures on the class of graphs of treewidth at most k, improve significantly on theoretical upper bounds obtained using previously available techniques.