From Width-Based Model Checking to Width-Based Automated Theorem Proving
Authors: Mateus de Oliveira Oliveira, Farhad Vadiee
AAAI 2023 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | 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. |
| Researcher Affiliation | Academia | Mateus de Oliveira Oliveira1,2, Farhad Vadiee2 1 Department of Computer and System Sciences, Stockholm University, Stockholm, Sweden 2 Department of Informatics, University of Bergen, Bergen, Norway |
| Pseudocode | No | The paper does not contain structured pseudocode or algorithm blocks. |
| Open Source Code | No | The paper does not provide concrete access to source code for the methodology described. |
| Open Datasets | No | The paper is theoretical and does not conduct experiments with datasets, so it does not specify public availability of training data. |
| Dataset Splits | No | The paper is theoretical and does not conduct experiments with datasets, so it does not provide dataset splits. |
| Hardware Specification | No | The paper is theoretical and does not describe experimental procedures that would require hardware specifications. |
| Software Dependencies | No | The paper is theoretical and does not describe experimental procedures that would require software dependencies with version numbers. |
| Experiment Setup | No | The paper is theoretical and does not describe experimental setups, hyperparameters, or training configurations. |