arXiv++ Combinatorics

Width-based automated theorem proving is a framework where counterexamples to graph-theoretic conjectures are searched width-wise relative to some graph width measure, such as treewidth or pathwidth. In a recent work it has been shown that dynamic programming algorithms operating on tree decompositions can be combined together with the purpose of width-based theorem proving. This approach can be used to show that several long-standing conjectures in graph theory can be tested in time \(2^{2^{k^{O(1)}}}\) on the class of graphs of treewidth at most \(k\). In this work, we give the first steps towards evaluating the viability of this framework from a practical standpoint. At the same time, we advance the framework in two directions. First, we introduce a state-canonization technique that significantly reduces the number of states evaluated during the search for a counterexample of the conjecture. Second, we introduce an early-pruning technique that can be applied in the study of conjectures of the form \(\mathcal{P}_1 \rightarrow \mathcal{P}_2\), for graph properties \(\mathcal{P}_1\) and \(\mathcal{P}_2\), where \(\mathcal{P}_1\) is a property closed under subgraphs. As a concrete application, we use our framework in the study of graph-theoretic conjectures related to coloring triangle-free graphs. In particular, our algorithm is able to show that Reed's conjecture for triangle-free graphs is valid on the class of graphs of pathwidth at most 5, and on graphs of treewidth at most 3. Perhaps more interestingly, our algorithm is able to construct in a completely automated way counterexamples to invalid strengthenings of Reed's conjecture. These are the first results showing that width-based automated theorem proving is a promising avenue in the study of graph-theoretic conjectures.

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.