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


  • Mateus de Oliveira Oliveira Stockholm University University of Bergen
  • Farhad Vadiee University of Bergen



KRR: Computational Complexity of Reasoning, KRR: Automated Reasoning and Theorem Proving


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 a polynomial of k 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.




How to Cite

de Oliveira Oliveira, M., & Vadiee, F. (2023). From Width-Based Model Checking to Width-Based Automated Theorem Proving. Proceedings of the AAAI Conference on Artificial Intelligence, 37(5), 6297-6304.



AAAI Technical Track on Knowledge Representation and Reasoning