Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
From Width-Based Model Checking to Width-Based Automated Theorem Proving
Stockholm University, Faculty of Social Sciences, Department of Computer and Systems Sciences. University of Bergen.
University of Bergen.
Number of Authors: 22023 (English)In: Proceedings of the AAAI Conference on Artificial Intelligence: AAAI-23 Technical Tracks 5 / [ed] Brian Williams; Yiling Chen; Jennifer Neville, AAAI Press , 2023, Vol. 37(5), p. 6297-6304Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
AAAI Press , 2023. Vol. 37(5), p. 6297-6304
Series
Proceedings of the ... AAAI Conference on Artificial Intelligence, ISSN 2159-5399, E-ISSN 2374-3468
Keywords [en]
KRR: Computational Complexity of Reasoning, KRR: Automated Reasoning and Theorem Proving
National Category
Computer Sciences
Research subject
Computer and Systems Sciences
Identifiers
URN: urn:nbn:se:su:diva-225842DOI: 10.1609/AAAI.V37I5.25775Scopus ID: 2-s2.0-85167867111ISBN: 978-1-57735-880-0 (print)OAI: oai:DiVA.org:su-225842DiVA, id: diva2:1830696
Conference
The Thirty-Seventh AAAI Conference on Artificial Intelligence was held on February 7–14, 2023 in Washington, D.C., USA.
Available from: 2024-01-23 Created: 2024-01-23 Last updated: 2024-10-16Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

De Oliveira Oliveira, Mateus

Search in DiVA

By author/editor
De Oliveira Oliveira, Mateus
By organisation
Department of Computer and Systems Sciences
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 83 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf