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.

翻译：基于宽度的自动定理证明是一种框架，其中对图论猜想的反例搜索基于某种图宽度度量（如树宽或路径宽）按宽度方向进行。近期研究表明，基于树分解的动态规划算法可与宽度定理证明相结合，这一方法可证明图论中多个长期悬而未决的猜想可在树宽不超过 \(k\) 的图类上以 \(2^{2^{k^{O(1)}}}\) 时间进行检验。本文首次从实践角度评估该框架的可行性，同时从两个方向推进该框架：首先，引入状态规范化技术，显著减少猜想反例搜索过程中需评估的状态数量；其次，针对形如 \(\mathcal{P}_1 \rightarrow \mathcal{P}_2\)（其中 \(\mathcal{P}_1\) 为子图封闭性质）的猜想研究，提出一种早期剪枝技术。作为具体应用，我们将该框架用于与三染色无三角形图相关的图论猜想研究。具体而言，我们的算法能够证明：Reed猜想关于无三角形图的部分在路径宽不超过5的图类及树宽不超过3的图类中成立。更值得关注的是，算法能以全自动方式构造Reed猜想强化版本的反例。这些首次结果表明，基于宽度的自动定理证明是研究图论猜想的一个有前景的途径。