Pith. sign in

REVIEW 7 minor 125 references

Advances in Algorithmic Meta Theorems

T0 review · 0 major / 7 minor · reviewed 2026-08-12 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Monadic dependence is the conjectured frontier of FO model checking.

desk verdict A reliable, well-flagged survey of algorithmic meta theorems; no new results, but it earns its place as a current map if the authors add preprint warnings. read the letter →

arxiv 2411.15365 v1 pith:4TFCIWOX submitted 2024-11-22 cs.LO cs.DMmath.COmath.LO

Sebastian Siebertz , Alexandre Vigny This is my paper · ORCID
classification cs.LOcs.DMmath.COmath.LO MSC 03C4503C1305C8568Q19
keywords algorithmicmetatheoremsmodelcheckingfixed-parametertractabilitymonadicstabilitydependencetwinwidthfirst-orderlogicsecond-order
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This survey maps the current frontier of algorithmic meta theorems—results of the form 'every problem expressible in a logic L can be solved efficiently on every class C of structures satisfying certain conditions.' Its central claim is that the field has converged on a conjectured dividing line: on hereditary graph classes, first-order (FO) model checking should be fixed-parameter tractable exactly when the class is monadically dependent, a model-theoretic tameness notion. The paper reports the two advances that make this frontier visible: a combinatorial structure theory for monadically stable classes and the width measure twinwidth, plus new logics between FO and MSO that unify techniques such as the irrelevant vertex method and recursive understanding. It also sketches the proofs of the main recent theorems, giving a reader an accurate picture of what is known and what remains open.

What carries the argument

The paper organizes the area around a small set of reduction methods—interpretation, composition, automata, locality with games, and quantifier elimination—and adds three newer tools that carry the recent results: the Flipper game and sparse r-neighborhood covers, which recursively simplify local neighborhoods on monadically stable classes; twinwidth, defined by contraction sequences whose width bounds the impurity of quotient trigraphs and along which dynamic programming tracks local types; and unbreakable tree decompositions combined with the irrelevant vertex technique, which reduce logics like CMSO/tw+dp to CMSO on bounded treewidth. These mechanisms are what the survey sketches as the proofs of the frontier theorems.

What would settle it

A hereditary class of graphs that is monadically dependent but on which FO model checking is W[1]-hard (parameterized by formula length) would refute the conjecture that monadic dependence marks the tractability boundary; no such class is currently known.

Watch

Extended reading notes

Core claim

The paper's thesis is that algorithmic meta theorems have reached a new stage: while CMSO model checking is essentially settled, and FO model checking on monotone classes is fully explained by nowhere denseness, the open frontier for FO model checking lies on hereditary classes, where the conjectured tractability boundary is monadic dependence. It presents the recent proof that FO model checking is fixed-parameter tractable on monadically stable classes, via the Flipper game and sparse neighborhood covers; the twinwidth framework, which makes FO model checking tractable on classes with bounded twinwidth given a contraction sequence and exactly captures monadic dependence on ordered classes; and the new intermediate logics, including separator logic, disjoint-paths logic, compound logic, and CMSO/tw+dp, which reduce model checking to CMSO on bounded treewidth or to FO on augmented trees. The paper thereby aims to establish that these results form a coherent picture: recursive decomposition of local neighborhoods, compositional reduction to unbreakable parts, and dynamic programming along contraction sequences are the modern replacements for the classical toolbox of automata, locality, and quantifier elimination.

Load-bearing premise

The survey's picture of the frontier depends on the correctness of the primary results it cites, especially FO model checking on monadically stable classes and the reduction of CMSO/tw+dp on minor-closed classes to CMSO on bounded treewidth, whose proofs are only sketched here.

Editorial extensions

If this is right

  • On ordered graphs the conjecture is already settled: a hereditary class of ordered graphs has bounded twinwidth if and only if it is monadically dependent, and FO model checking is fixed-parameter tractable there, giving a complete dichotomy for ordered hereditary classes.
  • FO model checking is fixed-parameter tractable on every monadically stable class, extending the nowhere dense result to a strictly larger family that includes dense graphs.
  • Model checking for CMSO/tw+dp is fixed-parameter tractable on every minor-closed class, since it reduces to CMSO on classes of bounded treewidth.
  • Separator logic and disjoint-paths logic are fixed-parameter tractable on classes with excluded topological minors, via automata on augmented trees and composition over unbreakable decompositions.
  • If the monadic dependence conjecture holds, then a hereditary class admits efficient FO model checking if and only if it is monadically dependent, giving a sharp algorithmic dividing line for all hereditary classes.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The conjecture suggests a hereditary analogue of the nowhere dense barrier: monadically dependent classes would be exactly the algorithmically tame hereditary classes, while every other hereditary class interprets all graphs and is thus intractable under standard assumptions.
  • A natural route to extending the game-based method is to find a game for monadically dependent classes that, combined with sparse neighborhood covers, yields a bounded-size recursive data structure; a testable intermediate step is whether monadically dependent classes admit r-neighborhood covers of degree n^epsilon for every epsilon greater than zero.
  • The intermediate logics between FO and CMSO suggest a spectrum of tractable logics indexed by how much set quantification is allowed, with CMSO/tw as a calibrated fragment; this could yield a fine-grained hierarchy of algorithmic meta theorems rather than a single boundary.
  • Since bounded twinwidth is preserved under FO transductions and captures monadic dependence on ordered classes, a promising route to the full conjecture is to prove that every monadically dependent hereditary class admits a twinwidth-like contraction sequence computable in fixed-parameter tractable time without an ordering.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

0 major / 7 minor

Summary. This survey reviews recent algorithmic meta theorems for model checking, with emphasis on FO model checking on hereditary graph classes and on logics between FO and MSO. It covers the interpretation/reduction method, quantifier elimination, the composition method, automata on augmented trees, locality and game-based decompositions, and twinwidth. The central results reported include FPT model checking for FO on nowhere dense and monadically stable classes (Theorems 9.1 and 9.2), the ordered twinwidth/monadic-dependence equivalence and its algorithmic consequences (Section 10), and reductions for separator logic, disjoint-paths logic, and CMSO/tw+dp on minor- and topological-minor-free classes (Theorems 4.2-4.4 and Corollary 7.1). The paper positions monadic dependence as the conjectured tractability boundary for FO on hereditary classes and clearly identifies the main open problems, in particular the extension of the game-based approach from monadically stable to monadically dependent classes.

Significance. If accurate, this is a useful and timely survey: it connects model-theoretic dividing lines (monadic stability and dependence) with algorithmic width measures (twinwidth) and with concrete logics (FO+conn, FO+dp, CMSO/tw). Its strengths include careful attribution to primary sources, explicit statements of limitations, and honest labeling of proof sketches as rough. In particular, the paper explicitly flags the bag-graph obstruction to extending the automata method to nowhere dense classes (Section 8), the non-uniform nature of the recursive-understanding reduction (Section 7), and the fact that the irrelevant-vertex reduction for CMSO/tw+dp rewrites the formula rather than producing a logically equivalent bounded-treewidth graph (Section 4.2). The external-dependency concern about Theorem 9.2 resting on the arXiv preprint [41] is, on reading the paper, an ordinary survey dependency rather than an internal flaw: the paper labels its expositions as sketches and independently cites the Flipper-game characterization to the peer-reviewed [65]; a reader wanting full verification is directed to the primary literature.

minor comments (7)
  1. [References] Many reference entries contain corrupted author names caused by stray LaTeX control sequences, e.g., "Micha/suppress l" in [22, 31, 32, 33, 41, 49, 96] and "Pawe/suppress l" in [32]; these need to be cleaned before publication.
  2. [Section 5.1, Lemma 5.1] The last sentence of Lemma 5.1 says "ψ can be efficiently computed from ψ”; this should read "ψ can be efficiently computed from φ.”
  3. [Section 4.2 and Theorem 8.4] There are several grammatical slips: "Another logic recently introduced logic by Sau" should be rephrased, and Theorem 8.4 says "Let C be a class excluded a topological minor" instead of "excluding a topological minor.”
  4. [Section 8] In the paragraph on bag graphs, "we need to toke the so-called bag graphs" should read "we need to take the so-called bag graphs.”
  5. [Section 2.7] The one-sentence claim that the hardness part of the monadic-dependence conjecture was established in [46] would be easier to verify if the exact hardness statement were quoted, since the title of [46] emphasizes a combinatorial dichotomy rather than an algorithmic lower bound.
  6. [Section 9.3, Theorem 9.2] Since the r-neighborhood cover lemma for monadically stable classes is attributed to the arXiv preprint [41], a brief remark stating that this is the key unreviewed dependency, while the Flipper-game characterization is covered by the peer-reviewed [65], would help readers calibrate confidence in the frontier statement.
  7. [Throughout] The paper alternates between "twinwidth" and "twin-width”; one consistent spelling should be chosen. There is also a typo "treewdith” in Section 3.4.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: survey exposition of independently cited theorems; no prediction reduces to its inputs.

full rationale

This paper is a survey of algorithmic meta theorems, not a derivation of new results. Its central claims are of the form 'Theorem X ([refs]) is FPT', and the proofs are explicitly rough sketches ('The theorem is proved using the irrelevant vertex technique...', 'we only give a very rough sketch and refer to the literature'). The only load-bearing external dependencies, such as Theorem 9.2 ('Let C be a monadically stable class. Then MC(FO, C) is fixed-parameter tractable') citing [44] and [41], are citations to published or preprint primary sources rather than to conclusions derived from the survey's own definitions. While several of those sources share authors with this survey (e.g., [44], [106], [112], [113]), that self-citation is normal scholarly practice and does not make the survey's exposition circular: the cited works are independent peer-reviewed results, and the survey does not fit a parameter, rename a known result, or define its objects in terms of its conclusions. The reliance on the unreviewed arXiv preprint [41] for part of Theorem 9.2 is a genuine verification risk, but that is an external-dependency concern, not a circularity, and per the review rules it does not raise the circularity score.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

The survey's accuracy rests on the correctness of the cited primary results and on standard background definitions. No free parameters are fitted and no new entities are postulated.

assumptions (3)
  • domain assumption The cited primary theorems are correct as stated.
    The survey's reliability depends on the accuracy of its sources, e.g., Theorem 9.2 [44,41], Theorem 4.3 [111], Theorem 4.2 [106]. These results are not proved in the paper.
  • standard math Standard definitions and conventions of finite model theory and parameterized complexity.
    Section 3 fixes FO, MSO, CMSO, treewidth, and FPT; the survey relies on these as background without re-deriving them.
  • domain assumption Complexity-theoretic assumptions used to state intractability limits (e.g., ETH, W-hierarchy conjectures).
    Statements such as 'assuming ETH, this running time cannot be improved' (Section 2.3) are cited from prior work and used as framing, not proved here.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Advances in Algorithmic Meta Theorems." pith.science (2026). https://pith.science/paper/4TFCIWOX

@misc{pith2026241115365,
  author       = {Pith},
  title        = {Pith review of: Advances in Algorithmic Meta Theorems},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/4TFCIWOX}},
  note         = {Machine review of arXiv:2411.15365}
}
abstract

Tractability results for the model checking problem of logics yield powerful algorithmic meta theorems of the form: Every computational problem expressible in a logic $L$ can be solved efficiently on every class $\mathscr{C}$ of structures satisfying certain conditions. The most prominent logics studied in the field are (counting) monadic second-order logic (C)MSO, and first-order logic FO and its extensions. The complexity of CMSO model checking in general and of FO model checking on monotone graph classes is very well understood. In recent years there has been a rapid and exciting development of new algorithmic meta theorems. On the one hand there has been major progress for FO model checking on hereditary graph classes. This progress was driven by the development of a combinatorial structure theory for the logically defined monadically stable and monadically dependent graph classes, as well as by the advent of the new width measure twinwidth. On the other hand, new algorithmic meta theorems for new logics with expressive power between FO and CMSO offer a new unifying view on methods like the irrelevant vertex technique and recursive understanding. In this paper we overview the recent advances in algorithmic meta theorems and provide rough sketches for the methods to prove them.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

125 extracted references · 74 canonical work pages

  1. [44]

    First-order model checking on struc- turally sparse graph classes

    Jan Dreier, Nikolas M¨ ahlmann, and Sebastian Siebertz. First-order model checking on struc- turally sparse graph classes. In Proceedings of the 55th Annual ACM Symposium on Theory of Computing , pages 567–580, 2023

    2023

  2. [41]

    First-order model checking on monadically stable graph classes

    Jan Dreier, Ioannis Eleftheriadis, Nikolas M¨ ahlmann, Rose McCarty, Micha/suppress l Pilipczuk, and Szymon Toru´ nczyk. First-order model checking on monadically stable graph classes. arXiv preprint arXiv:2311.18740, 2023

    arXiv 2023

  3. [111]

    Parameterizing the quantification of cmso: model checking on minor-closed graph classes

    Ignasi Sau, Giannos Stamoulis, and Dimitrios M Thilik os. Parameterizing the quantification of cmso: model checking on minor-closed graph classes. arXiv preprint arXiv:2406.18465 , 2024. 32

    arXiv 2024

  4. [65]

    Flip- per games for monadically stable graph classes

    Jakub Gajarsk´ y, Nikolas M¨ ahlmann, Rose McCarty, Pierre Ohlmann, Michal Pilipczuk, Wo- jciech Przybyszewski, Sebastian Siebertz, Marek Sokolows ki, and Szymon Torunczyk. Flip- per games for monadically stable graph classes. In 50th International Colloquium on Au- tomata, Languages, and Programming, ICALP 2023 , volume 261 of LIPIcs, pages 128:1– 128:16...

    work page 2023

  5. [1]

    Interpreting nowhere dense graph classes as a classical notion of model theory

    Hans Adler and Isolde Adler. Interpreting nowhere dense graph classes as a classical notion of model theory. European Journal of Combinatorics , 36:322–330, 2014

    2014

  6. [2]

    Second-order quantifi ers and the complexity of theories

    John T Baldwin and Saharon Shelah. Second-order quantifi ers and the complexity of theories. Notre Dame Journal of Formal Logic , 26(3):229–303, 1985

    1985

  7. [3]

    On uniformity within NC1

    David A Mix Barrington, Neil Immerman, and Howard Straub ing. On uniformity within NC1. Journal of Computer and System Sciences , 41(3):274–306, 1990

    1990

  8. [4]

    Expressive power of unary counters

    Michael Benedikt and H Jerome Keisler. Expressive power of unary counters. Structures in Logic and Computer Science: A Selection of Essays in Honor of A. Ehrenfeucht, pages 34–50, 2005

    2005

Show all 125 references
  1. [5]

    Separator logic and star-free expre ssions for graphs

    Mikolaj Bojanczyk. Separator logic and star-free expre ssions for graphs. arXiv preprint arXiv:2107.13953, 2021

    2021 arXiv

  2. [6]

    Twin-width VIII: delineation and Win- Wins

    ´Edouard Bonnet, Dibyayan Chakraborty, Eun Jung Kim, Noleen K¨ ohler, Raul Lopes, and St´ ephan Thomass´ e. Twin-width VIII: delineation and Win- Wins. In 17th International Symposium on Parameterized and Exact Computation, IPEC 202 2, volume 249 of LIPIcs, pages 9:1–9:18. Sch...

    2022

  3. [7]

    Model checking on interpreta tions of classes of bounded local cliquewidth

    ´Edouard Bonnet, Jan Dreier, Jakub Gajarsk` y, Stephan Kreutzer, Nikolas M¨ ahlmann, Pierre Simon, and Szymon Toru´ nczyk. Model checking on interpreta tions of classes of bounded local cliquewidth. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic i n Computer Sci...

    2022

  4. [8]

    Twin-width II: small classes

    ´Edouard Bonnet, Colin Geniet, Eun Jung Kim, St´ ephan Thomas s´ e, and R´ emi Watrigant. Twin-width II: small classes. In Proceedings of the 2021 ACM-SIAM Symposium on Discrete Algorithms (SODA), pages 1977–1996. SIAM, 2021

    2021

  5. [9]

    Twin-width III: max independent set, min dominating set, and coloring

    ´Edouard Bonnet, Colin Geniet, Eun Jung Kim, St´ ephan Thomas s´ e, and R´ emi Watrigant. Twin-width III: max independent set, min dominating set, and coloring. In 48th International Colloquium on Automata, Languages, and Programming, ICALP 2021, volume 198 of LIPIcs, pages 35...

    2021

  6. [10]

    Twin-width IV: ordered graphs and matrices

    ´Edouard Bonnet, Ugo Giocanti, Patrice Ossona de Mendez, Pierre Simon, St´ ephan Thomass´ e, and Szymon Toru´ nczyk. Twin-width IV: ordered graphs and matrices. Journal of the ACM , 71(3):1–45, 2024

    2024

  7. [11]

    Twin- width V: linear minors, modular counting, and matrix multip lication

    ´Edouard Bonnet, Ugo Giocanti, Patrice Ossona de Mendez, and St´ ephan Thomass´ e. Twin- width V: linear minors, modular counting, and matrix multip lication. In 40th International Symposium on Theoretical Aspects of Computer Science, STAC S 2023, volume 254 of LIPIcs, pages 1...

    2023

  8. [12]

    Twin-width VI: the lens of contraction sequences

    ´Edouard Bonnet, Eun Jung Kim, Amadeus Reinald, and St´ ephanThomass´ e. Twin-width VI: the lens of contraction sequences. In SODA, pages 1036–1056. SIAM, 2022

    2022

  9. [13]

    Twin-width and polynomial kernels

    ´Edouard Bonnet, Eun Jung Kim, Amadeus Reinald, St´ ephan Thomass´ e, and R´ emi Watrigant. Twin-width and polynomial kernels. Algorithmica, 84(11):3300–3337, 2022

    2022

  10. [14]

    Twin-width I: tractable FO model checking

    ´Edouard Bonnet, Eun Jung Kim, St´ ephan Thomass´ e, and R´ emiWatrigant. Twin-width I: tractable FO model checking. ACM Journal of the ACM (JACM) , 69(1):1–46, 2021

    2021

  11. [15]

    Twin-width and permutations.Logical Methods in Computer Science , 20, 2024

    ´Edouard Bonnet, Jaroslav Neˇ setˇ ril, Patrice Ossona de Men dez, Sebastian Siebertz, and St´ ephan Thomass´ e. Twin-width and permutations.Logical Methods in Computer Science , 20, 2024

    2024

  12. [16]

    Existential characterizations of monadic NIP

    Samuel Braunfeld and Michael C Laskowski. Existential characterizations of monadic NIP. arXiv preprint arXiv:2209.05120 , 2022

    2022

  13. [18]

    De- composition horizons and a characterization of stable here ditary classes of graphs

    Samuel Braunfeld, Jaroslav Neˇ setˇ ril, Patrice Ossona de Mendez, and Sebastian Siebertz. De- composition horizons and a characterization of stable here ditary classes of graphs. arXiv preprint arXiv:2209.11229, 2024

    2024 arXiv

  14. [19]

    Structure and complexit y of relational queries

    Ashok Chandra and David Harel. Structure and complexit y of relational queries. Journal of Computer and system Sciences , 25(1):99–128, 1982

    1982

  15. [20]

    Optimal implementa tion of conjunctive queries in relational data bases

    Ashok K Chandra and Philip M Merlin. Optimal implementa tion of conjunctive queries in relational data bases. In Proceedings of the ninth annual ACM symposium on Theory of computing, pages 77–90, 1977. 26

    1977

  16. [21]

    Stro ng computational lower bounds via parameterized complexity

    Jianer Chen, Xiuzhen Huang, Iyad A Kanj, and Ge Xia. Stro ng computational lower bounds via parameterized complexity. Journal of Computer and System Sciences , 72(8):1346–1367, 2006

    2006

  17. [22]

    Designing fpt algorithms for cut problems using randomized contractions

    Rajesh Chitnis, Marek Cygan, MohammadTaghi Hajiaghay i, Marcin Pilipczuk, and Micha/suppress l Pilipczuk. Designing fpt algorithms for cut problems using randomized contractions. SIAM Journal on Computing , 45(4):1171–1229, 2016

    2016

  18. [23]

    A relational model of data for large shared data banks

    Edgar F Codd. A relational model of data for large shared data banks. Communications of the ACM, 13(6):377–387, 1970

    1970

  19. [24]

    A combinatorial theorem for trees: a pplications to monadic logic and in- finite structures

    Thomas Colcombet. A combinatorial theorem for trees: a pplications to monadic logic and in- finite structures. In Automata, Languages and Programming: 34th International C olloquium, ICALP 2007 , pages 901–912. Springer, 2007

    2007

  20. [25]

    Graph rewriting: An algebraic and log ic approach

    Bruno Courcelle. Graph rewriting: An algebraic and log ic approach. In Formal models and semantics, pages 193–242. Elsevier, 1990

    1990

  21. [26]

    The monadic second-order logic of gra phs

    Bruno Courcelle. The monadic second-order logic of gra phs. I. Recognizable sets of finite graphs. Information and computation , 85(1):12–75, 1990

    1990

  22. [27]

    The monadic second-order logic of gra phs VII: Graphs as relational struc- tures

    Bruno Courcelle. The monadic second-order logic of gra phs VII: Graphs as relational struc- tures. Theoretical Computer Science, 101(1):3–33, 1992

    1992

  23. [28]

    Lin ear time solvable optimization problems on graphs of bounded clique-width

    Bruno Courcelle, Johann A Makowsky, and Udi Rotics. Lin ear time solvable optimization problems on graphs of bounded clique-width. Theory of Computing Systems , 33(2):125–150, 2000

    2000

  24. [29]

    Upper bounds to the clique width of graphs

    Bruno Courcelle and Stephan Olariu. Upper bounds to the clique width of graphs. Discrete Applied Mathematics, 101(1-3):77–114, 2000

    2000

  25. [30]

    Vertex-minors, monad ic second-order logic, and a conjec- ture by Seese

    Bruno Courcelle and Sang-il Oum. Vertex-minors, monad ic second-order logic, and a conjec- ture by Seese. Journal of Combinatorial Theory, Series B , 97(1):91–126, 2007

    2007

  26. [31]

    Springer, 2015

    Marek Cygan, Fedor V Fomin, /suppress Lukasz Kowalik, Daniel Lokshtanov, D´ aniel Marx, Marcin Pilipczuk, Micha/suppress l Pilipczuk, and Saket Saurabh.Parameterized algorithms , volume 5. Springer, 2015

    2015

  27. [32]

    Randomized contractions meet lean decompositions

    Marek Cygan, Pawe/suppress l Komosa, Daniel Lokshtanov, MarcinPilipczuk, Micha/suppress l Pilipczuk, Saket Saurabh, and Magnus Wahlstr¨ om. Randomized contractions meet lean decompositions. ACM Transactions on Algorithms (TALG) , 17(1):1–30, 2020

    2020

  28. [33]

    Minimum bisection is fixed parameter tractable

    Marek Cygan, Daniel Lokshtanov, Marcin Pilipczuk, Mic ha/suppress l Pilipczuk, and Saket Saurabh. Minimum bisection is fixed parameter tractable. In Proceedings of the forty-sixth annual ACM symposium on Theory of computing , pages 323–332, 2014

    2014

  29. [34]

    Minimum bisection is fixed-parameter tractable

    Marek Cygan, Daniel Lokshtanov, Marcin Pilipczuk, Mic ha/suppress l Pilipczuk, and Saket Saurabh. Minimum bisection is fixed-parameter tractable. SIAM Journal on Computing , 48(2):417–450, 2019

    2019

  30. [35]

    Locall y excluding a minor

    Anuj Dawar, Martin Grohe, and Stephan Kreutzer. Locall y excluding a minor. In LICS 2007, pages 270–279. IEEE, 2007. 27

    2007

  31. [36]

    Tree acceptors and some of their applicatio ns

    John Doner. Tree acceptors and some of their applicatio ns. Journal of Computer and System Sciences, 4(5):406–451, 1970

    1970

  32. [37]

    Fixed-parameter tra ctability and completeness I: Basic results

    Rod G Downey and Michael R Fellows. Fixed-parameter tra ctability and completeness I: Basic results. SIAM Journal on computing , 24(4):873–921, 1995

    1995

  33. [38]

    Downey and Michael R

    Rodney G. Downey and Michael R. Fellows. Parameterized Complexity . Monographs in Computer Science. Springer, 1999

    1999

  34. [39]

    Fundamentals of parameterized complexity , volume 4

    Rodney G Downey, Michael R Fellows, et al. Fundamentals of parameterized complexity , volume 4. Springer, 2013

    2013

  35. [40]

    Lacon-and shrub-decompositions: A new cha racterization of first-order transduc- tions of bounded expansion classes

    Jan Dreier. Lacon-and shrub-decompositions: A new cha racterization of first-order transduc- tions of bounded expansion classes. In 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) , pages 1–13. IEEE, 2021

    2021

  36. [42]

    Tree- like decompositions for transductions of sparse graphs

    Jan Dreier, Jakub Gajarsk` y, Sandra Kiefer, Micha/suppress l Pilipczuk, and Szymon Toru´ nczyk. Tree- like decompositions for transductions of sparse graphs. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science , pages 1–14, 2022

    2022

  37. [43]

    Mouawad, Sebastian Siebertz, and Alexandre Vigny

    Jan Dreier, Nikolas M¨ ahlmann, Amer E. Mouawad, Sebastian Siebertz, and Alexandre Vigny. Combinatorial and algorithmic aspects of monadic stabilit y. In 33rd International Sympo- sium on Algorithms and Computation, ISAAC 2022 , volume 248 of LIPIcs, pages 11:1–11:17. Schloss ...

    2022

  38. [45]

    Indiscernibles and flatness in monadically stable and monadically nip class es

    Jan Dreier, Nikolas M¨ ahlmann, Sebastian Siebertz, an d Szymon Toru´ nczyk. Indiscernibles and flatness in monadically stable and monadically nip class es. In 50th International Collo- quium on Automata, Languages, and Programming (ICALP 2023) . Schloss-Dagstuhl-Leibniz Zentru...

    2023

  39. [46]

    In Proceedings of the 56th Annual ACM Symposium on Theory of Computing , pages 1550–1560, 2024

    Jan Dreier, Nikolas M¨ ahlmann, and Szymon Toru´ nczyk.Flip-breakability: A combinatorial dichotomy for monadically dependent graph classes. In Proceedings of the 56th Annual ACM Symposium on Theory of Computing , pages 1550–1560, 2024

    2024

  40. [47]

    Deciding first-order properties for sparse graphs

    Zdenˇ ek Dvoˇ r´ ak, Daniel Kr´ al, and Robin Thomas. Deciding first-order properties for sparse graphs. In 2010 IEEE 51st Annual Symposium on Foundations of Computer S cience, pages 133–142. IEEE, 2010

    2010

  41. [48]

    Testing first-order properties for subclasses of sparse graphs

    Zdenˇ ek Dvoˇ r´ ak, Daniel Kr´ al, and Robin Thomas. Testing first-order properties for subclasses of sparse graphs. Journal of the ACM (JACM) , 60(5):36, 2013

    2013

  42. [49]

    Perspectives in Mathematical Logic

    Heinz-Dieter Ebbinghaus and J¨ org Flum.Finite model theory. Perspectives in Mathematical Logic. Springer, 1995. 28

    1995

  43. [50]

    Mathematical logic (2

    Heinz-Dieter Ebbinghaus, J¨ org Flum, and Wolfgang Tho mas. Mathematical logic (2. ed.) . Undergraduate texts in mathematics. Springer, 1994

    1994

  44. [51]

    Model-checking on ordered structures

    Kord Eickmeyer, Jan van den Heuvel, Ken-ichi Kawarabay ashi, Stephan Kreutzer, Patrice Ossona De Mendez, Micha/suppress l Pilipczuk, Daniel A Quiroz, RomanRabinovich, and Sebastian Siebertz. Model-checking on ordered structures. ACM Transactions on Computational Logic (TOCL), ...

    2020

  45. [52]

    Counting quantifiers, successor rela tions, and logarithmic space

    Kousha Etessami. Counting quantifiers, successor rela tions, and logarithmic space. Journal of Computer and System Sciences , 54(3):400–411, 1997

    1997

  46. [53]

    Generalized first-order spectra and poly nomial-time recognizable sets

    Ronald Fagin. Generalized first-order spectra and poly nomial-time recognizable sets. Com- plexity of computation , 7:43–73, 1974

    1974

  47. [54]

    Monadic generalized spectra

    Ronald Fagin. Monadic generalized spectra. Math. Log. Q. , 21(1):89–96, 1975

    1975

  48. [55]

    The first order pro perties of products of algebraic systems

    Solomon Feferman and Robert L Vaught. The first order pro perties of products of algebraic systems. Journal of Symbolic Logic , 32(2), 1967

    1967

  49. [56]

    Fixed-parameter tractability, definability, and model-checking

    J¨ org Flum and Martin Grohe. Fixed-parameter tractability, definability, and model-checking. SIAM Journal on Computing , 31(1):113–145, 2001

    2001

  50. [57]

    Texts in Theoretical Com- puter Science

    J¨ org Flum and Martin Grohe.Parameterized Complexity Theory. Texts in Theoretical Com- puter Science. An EATCS Series. Springer, 2006

    2006

  51. [58]

    Compound logics for modification problems

    Fedor V Fomin, Petr A Golovach, Ignasi Sau, Giannos Stam oulis, and Dimitrios M Thilikos. Compound logics for modification problems. ACM Transactions on Computational Logic , 2023

    2023

  52. [59]

    An algo- rithmic meta-theorem for graph modification to planarity an d fol

    Fedor V Fomin, Petr A Golovach, Giannos Stamoulis, and D imitrios M Thilikos. An algo- rithmic meta-theorem for graph modification to planarity an d fol. ACM Transactions on Computation Theory, 14(3-4):1–29, 2023

    2023

  53. [60]

    Deciding first-order pro perties of locally tree-decomposable structures

    Markus Frick and Martin Grohe. Deciding first-order pro perties of locally tree-decomposable structures. Journal of the ACM (JACM) , 48(6):1184–1206, 2001

    2001

  54. [61]

    On local and non-local properties

    Haim Gaifman. On local and non-local properties. In Studies in Logic and the Foundations of Mathematics , volume 107, pages 105–135. Elsevier, 1982

    1982

  55. [62]

    A new perspective on FO model checking of dense graph cla sses

    Jakub Gajarsk` y, Petr Hlinˇ en` y, Jan Obdrˇ z´ alek, Daniel Lokshtanov, and M Sridharan Ramanu- jan. A new perspective on FO model checking of dense graph cla sses. ACM Transactions on Computational Logic (TOCL) , 21(4):1–23, 2020

    2020

  56. [63]

    Recovering sparse graphs

    Jakub Gajarsky and Daniel Kr´ al’ . Recovering sparse graphs. Leibniz International Proceedings in Informatics (LIPIcs) , 117:29, 2018

    2018

  57. [64]

    First-order interpretations of bounded expansion classes

    Jakub Gajarsk` y, Stephan Kreutzer, Jaroslav Neˇ setˇ ril, Patrice Ossona De Mendez, Micha/suppress l Pilipczuk, Sebastian Siebertz, and Szymon Toru´ nczyk. First-order interpretations of bounded expansion classes. ACM Transactions on Computational Logic (TOCL) , 21(4):1–41, 2020

    2020

  58. [66]

    Twin- width and types

    Jakub Gajarsk´ y, Michal Pilipczuk, Wojciech Przybyszewski, and Szymon Torunczyk. Twin- width and types. In 49th International Colloquium on Automata, Languages, and Program- ming, ICALP 2022 , volume 229 of LIPIcs, pages 123:1–123:21. Schloss Dagstuhl - Leibniz- Zentrum f¨ ur...

    2022

  59. [67]

    Stable graphs of bounded twin- width

    Jakub Gajarsk` y, Micha/suppress l Pilipczuk, and Szymon Toru´ nczyk. Stable graphs of bounded twin- width. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic i n Computer Science, pages 1–12, 2022

    2022

  60. [68]

    Lower bounds on the complexity of MSO 1 model-checking

    Robert Ganian, Petr Hlinˇ en` y, Alexander Langer, Jan Obdrˇ z´ alek, Peter Rossmanith, and Somnath Sikdar. Lower bounds on the complexity of MSO 1 model-checking. Journal of Computer and System Sciences , 80(1):180–194, 2014

    2014

  61. [69]

    Shrub-depth: Capturing height of dense graphs

    Robert Ganian, Petr Hlinˇ en` y, Jaroslav Neˇ setˇ ril, Jan Obdrˇ z´ alek, and Patrice Ossona De Mendez. Shrub-depth: Capturing height of dense graphs. Logical Methods in Computer Science, 15, 2019

    2019

  62. [70]

    When trees grow low: Shrubs and fast MSO1

    Robert Ganian, Petr Hlinˇ en` y, Jaroslav Neˇ setˇ ril, Jan Obdrˇ z´ alek, Patrice Ossona de Mendez, and Reshma Ramadurai. When trees grow low: Shrubs and fast MSO1. In Mathematical Foun- dations of Computer Science 2012: 37th International Sympo sium, MFCS 2012, Bratislava, S...

    2012

  63. [71]

    Order-invariant MSO is s tronger than counting MSO in the finite

    Tobias Ganzow and Sasha Rubin. Order-invariant MSO is s tronger than counting MSO in the finite. In Susanne Albers and Pascal Weil, editors, 25th Annual Symposium on Theoret- ical Aspects of Computer Science, STACS 2008 , volume 1 of LIPIcs, pages 313–324. Schloss Dagstuhl - Le...

    2008

  64. [72]

    Twin-Width, logical and combinatorial characterisations

    Colin Geniet. Twin-Width, logical and combinatorial characterisations . PhD thesis, Ecole normale sup´ erieure de lyon-ENS LYON, 2024

    2024

  65. [73]

    Model-checking for first-order logic with disjoint paths predicates in proper minor-close d graph classes

    Petr A Golovach, Giannos Stamoulis, and Dimitrios M Thilikos. Model-checking for first-order logic with disjoint paths predicates in proper minor-close d graph classes. In Proceedings of the 2023 Annual ACM-SIAM Symposium on Discrete Algorithms ( SODA), pages 3684–3699. SIAM, 2023

    2023

  66. [74]

    Springer, 2007

    Erich Gr¨ adel, Phokion G Kolaitis, Leonid Libkin, Maar ten Marx, Joel Spencer, Moshe Y Vardi, Yde Venema, Scott Weinstein, et al.Finite Model Theory and its applications . Springer, 2007

    2007

  67. [75]

    Discrepancy and sparsity

    Mario Grobler, Yiting Jiang, Patrice Ossona de Mendez, Sebastian Siebertz, and Alexandre Vigny. Discrepancy and sparsity. J. Comb. Theory B , 169:96–133, 2024

    2024

  68. [76]

    Logic, graphs, and algorithms

    Martin Grohe. Logic, graphs, and algorithms. Logic and automata , 2:357–422, 2008

    2008

  69. [77]

    Finding topolog- ical subgraphs is fixed-parameter tractable

    Martin Grohe, Ken-ichi Kawarabayashi, D´ aniel Marx, a nd Paul Wollan. Finding topolog- ical subgraphs is fixed-parameter tractable. In Proceedings of the forty-third annual ACM symposium on Theory of computing , pages 479–488, 2011

    2011

  70. [78]

    Methods for algorit hmic meta theorems

    Martin Grohe and Stephan Kreutzer. Methods for algorit hmic meta theorems. AMS-ASL Joint Special Session , 558:181–206, 2009

    2009

  71. [79]

    Deciding first-order properties of nowhere dense graphs

    Martin Grohe, Stephan Kreutzer, and Sebastian Siebert z. Deciding first-order properties of nowhere dense graphs. J. ACM, 64(3):17:1–17:32, 2017. 30

    2017

  72. [80]

    First-order quer y evaluation with cardinality condi- tions

    Martin Grohe and Nicole Schweikardt. First-order quer y evaluation with cardinality condi- tions. In Proceedings of the 37th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems , pages 253–266, 2018

    2018

  73. [81]

    Logic and the challenge of computer scie nce

    Yuri Gurevich. Logic and the challenge of computer scie nce. Technical report, 1985

    1985

  74. [82]

    Model theory, volume 42 of Encyclopedia of mathematics and its applications

    Wilfrid Hodges. Model theory, volume 42 of Encyclopedia of mathematics and its applications . Cambridge University Press, 1993

    1993

  75. [83]

    Upper and lower bounds for first order exp ressibility

    Neil Immerman. Upper and lower bounds for first order exp ressibility. Journal of Computer and System Sciences , 25(1):76–98, 1982

    1982

  76. [84]

    Languages that capture complexity clas ses

    Neil Immerman. Languages that capture complexity clas ses. SIAM J. Comput. , 16(4):760– 778, 1987

    1987

  77. [85]

    Descriptive complexity

    Neil Immerman. Descriptive complexity. Springer Science & Business Media, 1998

    1998

  78. [86]

    Regular partitions of gentle graphs

    Yiting Jiang, Jaroslav Neˇ setˇ ril, Patrice Ossona de Mendez, and Sebastian Siebertz. Regular partitions of gentle graphs. Acta Mathematica Hungarica , 161(2):719–755, 2020

    2020

  79. [87]

    The minimumk-way cut of bounded size is fixed- parameter tractable

    Ken-ichi Kawarabayashi and Mikkel Thorup. The minimumk-way cut of bounded size is fixed- parameter tractable. In 2011 IEEE 52nd Annual Symposium on Foundations of Computer Science, pages 160–169. IEEE, 2011

    2011

  80. [88]

    Algorithmic meta-theorems

    Stephan Kreutzer. Algorithmic meta-theorems. Finite and algorithmic model theory , 379:177– 270, 2011

    2011

  81. [89]

    On the parameterized intractabilit y of monadic second-order logic

    Stephan Kreutzer. On the parameterized intractabilit y of monadic second-order logic. Logical Methods in Computer Science , 8, 2012

    2012

  82. [90]

    Lower bounds for th e complexity of monadic second- order logic

    Stephan Kreutzer and Siamak Tazari. Lower bounds for th e complexity of monadic second- order logic. In 2010 25th Annual IEEE Symposium on Logic in Computer Science , pages 189–198. IEEE, 2010

    2010

  83. [91]

    On brambles, grid- like minors, and parameterized intractability of monadic second-order logic

    Stephan Kreutzer and Siamak Tazari. On brambles, grid- like minors, and parameterized intractability of monadic second-order logic. In Proceedings of the twenty-first annual ACM- SIAM symposium on Discrete Algorithms , pages 354–364. SIAM, 2010

    2010

  84. [92]

    First-order logic with counting

    Dietrich Kuske and Nicole Schweikardt. First-order logic with counting. In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) , pages 1–12. IEEE, 2017

    2017

  85. [93]

    Gaifman normal forms for counting extensions of first- order logic

    Dietrich Kuske and Nicole Schweikardt. Gaifman normal forms for counting extensions of first- order logic. In 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2018

    2018

  86. [94]

    Elements of finite model theory , volume 41

    Leonid Libkin. Elements of finite model theory , volume 41. Springer, 2004

    2004

  87. [95]

    Elements of Finite Model Theory

    Leonid Libkin. Elements of Finite Model Theory . Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004

    2004

  88. [96]

    Daniel Lokshtanov, M. S. Ramanujan, Saket Saurabh, and Meirav Zehavi. Reducing CMSO model checking to highly connected graphs. In 45th International Colloquium on Automata, Languages, and Programming, ICALP 2018 , volume 107 of LIPIcs, pages 135:1–135:14. Schloss Dagstuhl - Le...

    2018

  89. [97]

    PhD thesis, Universit¨ at Bremen, 2024

    Nikolas M¨ ahlmann.Monadically stable and monadically dependent graph classe s: character- izations and algorithmic meta-theorems . PhD thesis, Universit¨ at Bremen, 2024

    2024

  90. [98]

    Tree-width and the mona dic quantifier hierarchy

    Johann A Makowsky and JP Marino. Tree-width and the mona dic quantifier hierarchy. The- oretical computer science, 303(1):157–170, 2003

    2003

  91. [99]

    Regularity le mmas for stable graphs

    Maryanthe Malliaris and Saharon Shelah. Regularity le mmas for stable graphs. Transactions of the American Mathematical Society , 366(3):1551–1585, 2014

    2014

  92. [100]

    Structural sparsity

    Jaroslav Neˇ setˇ ril and P Ossona de Mendez. Structural sparsity. Russian Mathematical Sur- veys, 71(1):79, 2016

    2016

  93. [101]

    On n owhere dense graphs

    Jaroslav Neˇ setˇ ril and Patrice Ossona De Mendez. On n owhere dense graphs. European Journal of Combinatorics , 32(4):600–617, 2011

    2011

  94. [102]

    Rankwidth meets stability

    Jaroslav Neˇ setˇ ril, Patrice Ossona de Mendez, Micha/suppress l Pilipczuk, Roman Rabinovich, and Sebastian Siebertz. Rankwidth meets stability. In Proceedings of the 2021 ACM-SIAM Symposium on Discrete Algorithms (SODA) , pages 2014–2033. SIAM, 2021

    2021

  95. [103]

    Linear rankwidth meets stability

    Jaroslav Neˇ setˇ ril, Roman Rabinovich, Patrice Ossona de Mendez, and Sebastian Siebertz. Linear rankwidth meets stability. In Proceedings of the Fourteenth Annual ACM-SIAM Sym- posium on Discrete Algorithms , pages 1180–1199. SIAM, 2020

    2020

  96. [104]

    Canon- ical decompositions in monadically stable and bounded shru bdepth graph classes

    Pierre Ohlmann, Michal Pilipczuk, Wojciech Przybysz ewski, and Szymon Torunczyk. Canon- ical decompositions in monadically stable and bounded shru bdepth graph classes. In 50th International Colloquium on Automata, Languages, and Prog ramming, ICALP 2023 , volume 261 of LIPIcs...

    2023

  97. [105]

    Approximating clique-w idth and branch-width

    Sang-il Oum and Paul Seymour. Approximating clique-w idth and branch-width. Journal of Combinatorial Theory, Series B , 96(4):514–528, 2006

    2006

  98. [106]

    Algorithms and data structures for first-order lo gic with connectivity under ver- tex failures

    Michal Pilipczuk, Nicole Schirrmacher, Sebastian Si ebertz, Szymon Torunczyk, and Alexan- dre Vigny. Algorithms and data structures for first-order lo gic with connectivity under ver- tex failures. In 49th International Colloquium on Automata, Languages, and Programming, ICALP ...

    2022

  99. [107]

    Graph minors I – XXII I

    Neil Robertson and Paul D Seymour. Graph minors I – XXII I. 1983 - 2010

    1983

  100. [108]

    Graph minors

    Neil Robertson and Paul D Seymour. Graph minors. V. exc luding a planar graph. Journal of Combinatorial Theory, Series B , 41(1):92–114, 1986

    1986

  101. [109]

    Graph minors

    Neil Robertson and Paul D Seymour. Graph minors. XIII. the disjoint paths problem. Journal of combinatorial theory, Series B , 63(1):65–110, 1995

    1995

  102. [110]

    A more accurate view of the flat wall theorem

    Ignasi Sau, Giannos Stamoulis, and Dimitrios M Thilik os. A more accurate view of the flat wall theorem. Journal of Graph Theory , 107(2):263–297, 2024

    2024

  103. [112]

    Model checking disjoint-paths logic on topological-minor-free graph classes

    Nicole Schirrmacher, Sebastian Siebertz, Giannos St amoulis, Dimitrios M Thilikos, and Alexandre Vigny. Model checking disjoint-paths logic on topological-minor-free graph classes. In Proceedings of the 39th Annual ACM/IEEE Symposium on Logic i n Computer Science , pages 1–12, 2024

    2024

  104. [113]

    First-order logic with connec- tivity operators

    Nicole Schirrmacher, Sebastian Siebertz, and Alexan dre Vigny. First-order logic with connec- tivity operators. ACM Transactions on Computational Logic , 24(4):1–23, 2023

    2023

  105. [114]

    Arithmetic, first-order logic, and counting quantifiers

    Nicole Schweikardt. Arithmetic, first-order logic, and counting quantifiers. ACM Transactions on Computational Logic (TOCL) , 6(3):634–671, 2005

    2005

  106. [115]

    The structure of the models of decidable monadic theories of graphs

    Detlef Seese. The structure of the models of decidable monadic theories of graphs. Annals of pure and applied logic , 53(2):169–195, 1991

    1991

  107. [116]

    Linear time computable problems and firs t-order descriptions

    Detlef Seese. Linear time computable problems and firs t-order descriptions. Mathematical Structures in Computer Science , 6(6):505–526, 1996

    1996

  108. [117]

    Classification theory: and the number of non-isomorphic mod els

    Saharon Shelah. Classification theory: and the number of non-isomorphic mod els. Elsevier, 1990

    1990

  109. [118]

    The polynomial-time hierarchy

    Larry J Stockmeyer. The polynomial-time hierarchy. Theoretical Computer Science , 3(1):1– 22, 1976

    1976

  110. [119]

    The complexity of decision problems in automata theory and l ogic

    Larry Joseph Stockmeyer. The complexity of decision problems in automata theory and l ogic. PhD thesis, Massachusetts Institute of Technology, 1974

    1974

  111. [120]

    Thatcher and Jesse B

    James W. Thatcher and Jesse B. Wright. Generalized fini te automata theory with an appli- cation to a decision problem of second-order logic. Mathematical systems theory , 2(1):57–81, 1968

    1968

  112. [121]

    Excl uding surfaces as minors in graphs

    Dimitrios M Thilikos and Sebastian Wiederrecht. Excl uding surfaces as minors in graphs. arXiv preprint arXiv:2306.01724 , 2023

    2023 arXiv

  113. [122]

    Aggregate queries on sparse databases

    Szymon Toru´ nczyk. Aggregate queries on sparse databases. In Proceedings of the 39th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database S ystems, pages 427–443, 2020

    2020

  114. [123]

    Flip-width: Cops and robber on dense graphs

    Szymon Toru´ nczyk. Flip-width: Cops and robber on dense graphs. In 2023 IEEE 64th Annual Symposium on Foundations of Computer Science (FOCS) , pages 663–700. IEEE, 2023

    2023

  115. [124]

    The complexity of relational query languages

    Moshe Y Vardi. The complexity of relational query languages. In Proceedings of the fourteenth annual ACM symposium on Theory of computing , pages 137–146, 1982

    1982

  116. [125]

    Open problems from the workshop on algorithms, logic a nd structure, University of Warwick Workshop. 2016

    2016

  117. [126]

    Colouring graphs with bounded generalize d colouring number

    Xuding Zhu. Colouring graphs with bounded generalize d colouring number. Discrete Mathe- matics, 309(18):5562–5568, 2009. 33

    2009

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.