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

TL;DR

This paper introduces a modular framework that transforms width-based model checking algorithms into tools for testing graph-theoretic conjectures on bounded width graphs, providing new algorithmic bounds.

Contribution

It presents a general, modular framework for converting width-based model checking algorithms into algorithms for verifying graph conjectures on bounded width classes.

Findings

Algorithms for several conjectures run in double-exponential time in the width parameter.

The framework applies to multiple width measures like treewidth and cliquewidth.

Significant improvements in upper bounds for proof sizes of conjectures on bounded width graphs.

Abstract

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 $k^{O(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.