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

TL;DR

It is proved analytically that for several long-standing graph-theoretic conjectures, there exists an algorithm that correctly determines in time double-exponential in a polynomial of k whether the conjecture is valid on all graphs of treewidth at most k.

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.

Figures (2)

• Figure 1: A $2$-instructive tree decomposition $\tau$, and the graph $\mathcal{G}(\tau)$ associated with $\tau$. Note that the graph has four vertices even though only labels from the set $\{1,2,3\}$ are used in the instructions occurring in the tree. Intuitively, once a vertex has been forgotten, its label can be reused when introducing a new vertex.
• Figure 2: Construction of the graph associated to the $2$-instructive tree decomposition of Fig. \ref{['figure:TreeDecomposition']}. The set of active labels on each node is specified in blue, while the graph associated to the decomposition rooted at that node is specified in green. The boundary maps are omitted in the figure. Nevertheless, in each node the boundary map assigns each label $i$ to vertex $i$, except for the left child of the topmost node, where the boundary map assigns labels $1$, $2$, and $3$ to vertices $4$, $2$ and $3$ respectively.

Theorems & Definitions (40)

• Definition 2
• Definition 3: Treelike Width Measure
• Theorem 4
• Definition 5
• Lemma 6
• Definition 7: Treelike DP-Cores
• Definition 8: Dynamization
• Definition 9: Graph Property of a DP-Core
• Definition 10: Coherency
• Proposition 11