{"id":"arxiv/2605.11025","url":"https://arxiv.org/abs/2605.11025","tags":["cs.DS","cs.CC","cs.LO","math.CO"],"score":0,"title":"State Canonization and Early Pruning in Width-Based Automated Theorem Proving","domain":"cs.DS","source":"arxiv","authors":["Mateus de Oliveira Oliveira","Sam Urmian"],"reviews":0,"subject":"cs.DS","summary":"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…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-05-10","reactions":{}}