Journal Articles ACM Transactions on Computational Logic Year : 2024

Compound Logics for Modification Problems

Abstract

We introduce a novel model-theoretic framework inspired from graph modification and based on the interplay between model theory and algorithmic graph minors. The core of our framework is a new compound logic operating with two types of sentences, expressing graph modification: the modulator sentence, defining some property of the modified part of the graph, and the target sentence, defining some property of the resulting graph. In our framework, modulator sentences are in counting monadic second-order logic (CMSO) and have models of bounded treewidth, while target sentences express first-order logic (FO) properties. Our logic captures problems that are not definable in first-order logic and, moreover, may have instances of unbounded treewidth. Our main result is that, for this compound logic, model-checking can be done in quadratic time on minor-free graphs. The proposed logic can be seen as a general framework to capitalize on the potential of the irrelevant vertex technique. It gives a way to deal with problem instances of unbounded treewidth, for which Courcelle's theorem does not apply. The proof of our meta-theorem combines novel combinatorial results related to the Flat Wall theorem along with elements of the proof of Courcelle's theorem and Gaifman's theorem. Our algorithmic meta-theorem encompasses, unifies, and extends the known meta-algorithmic results for CMSO and FO on minor-closed graph classes.

Dates and versions

lirmm-04825119 , version 1 (07-12-2024)

Identifiers

Cite

Fedor V. Fomin, Petr A. Golovach, Ignasi Sau, Giannos Stamoulis, Dimitrios M. Thilikos. Compound Logics for Modification Problems. ACM Transactions on Computational Logic, 2024, Leibniz International Proceedings in Informatics (LIPIcs), 26 (1), pp.1-57. ⟨10.1145/3696451⟩. ⟨lirmm-04825119⟩
12 View
0 Download

Altmetric

Share

More