pith. sign in

arxiv: 2205.10995 · v3 · pith:JMJ3AMMEnew · submitted 2022-05-23 · 💻 cs.DS · cs.AI· cs.DM· cs.FL· cs.LO

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

Mateus de Oliveira Oliveira , Sam Urmian This is my paper

Pith reviewed 2026-05-24 11:54 UTC · model grok-4.3

classification 💻 cs.DS cs.AIcs.DMcs.FLcs.LO
keywords model checkingtheorem provingtreewidthcliquewidthgraph conjectureswidth measuresparameterized algorithmsbounded width
0
0 comments X

The pith

Several long-standing graph conjectures admit algorithms deciding their validity on all treewidth-at-most-k graphs in double-exponential time in k to a constant power.

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

The paper develops a general modular framework that converts a large class of width-based model-checking algorithms into algorithms that test whether graph-theoretic conjectures hold on every graph of bounded width. The framework works for standard measures including treewidth and cliquewidth. When the conversion is applied to known model-checking results, it produces, for several famous conjectures, a procedure that takes an integer k and decides in double-exponential time in k to a fixed power whether the conjecture is true for all graphs whose treewidth is at most k. These procedures supply explicit upper bounds on the length of any proof or disproof of the conjecture inside the class of low-treewidth graphs. A sympathetic reader would care because the new bounds are substantially tighter than those previously obtainable from general-purpose techniques.

Core claim

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

What carries the argument

The modular conversion framework that systematically transforms width-based model-checking procedures for combinatorial properties into conjecture-validation procedures for bounded-width graph classes while preserving parameterized running times.

If this is right

  • For several long-standing conjectures there exists an algorithm deciding validity on all graphs of treewidth at most k in time double-exponential in k to a constant power.
  • The conversion framework applies to multiple width measures including treewidth and cliquewidth.
  • The resulting procedures supply improved upper bounds on the size of proofs or disproofs for the conjectures inside bounded-width classes.
  • The framework is modular and applies to a large class of existing width-based model-checking algorithms.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The conversion technique could be tested on width measures other than treewidth and cliquewidth to see whether similar time bounds emerge.
  • The method suggests a route for building automated tools that exploit bounded width to verify additional graph properties beyond the conjectures treated in the paper.
  • One could examine whether the theoretical double-exponential procedures admit practical implementations that terminate quickly for small concrete values of k.

Load-bearing premise

That a large class of width-based model-checking algorithms can be systematically converted into algorithms that test the validity of graph-theoretic conjectures on classes of graphs of bounded width while preserving the required running-time bounds when applied to treewidth.

What would settle it

A specific long-standing graph conjecture together with a proof that no conversion from any width-based model-checking algorithm yields a correct decision procedure running in double-exponential time in k^{O(1)} on graphs of treewidth at most k.

Figures

Figures reproduced from arXiv: 2205.10995 by Mateus de Oliveira Oliveira, Sam Urmian.

Figure 1
Figure 1. Figure 1: Left: a 2-instructive tree decomposition [PITH_FULL_IMAGE:figures/full_fig_p007_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Construction of the graph associated to the 2-inst [PITH_FULL_IMAGE:figures/full_fig_p029_2.png] view at source ↗
read the original abstract

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 $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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper introduces a modular framework for converting a large class of width-based model-checking algorithms into procedures that test the validity of graph-theoretic conjectures on all graphs of bounded width (with respect to measures including treewidth and cliquewidth). As a quantitative application, it shows that several long-standing conjectures admit algorithms that, given k, decide validity on all graphs of treewidth at most k in time double-exponential in k^{O(1)}.

Significance. If the conversion framework and its runtime analysis hold, the work supplies a systematic bridge between width-based model checking and automated verification of conjectures on bounded-width classes, yielding improved upper bounds on proof/disproof sizes relative to prior techniques. The modularity across width measures and the preservation of double-exponential dependence on k are the primary contributions.

minor comments (2)
  1. [§1] §1 (Introduction): the statement that the new bounds 'improve significantly' on previous techniques would be strengthened by an explicit comparison (even a brief table) of the dependence on k obtained via the new framework versus the best prior generic methods.
  2. [§3] The framework description would benefit from a short pseudocode outline or diagram in §3 showing the exact steps of the conversion (encoding of the conjecture, invocation of the model checker, and extraction of the answer) to make the modularity claim easier to verify.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of the framework and its applications, as well as for recommending minor revision. The report does not raise any specific major comments.

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper introduces a new modular framework that converts existing width-based model-checking algorithms into procedures for testing graph-theoretic conjectures on bounded-width classes. The central quantitative claim follows directly from applying this framework to known model-checking routines on suitably encoded instances whose width remains linear in k, yielding the stated double-exponential runtime bound with no additional quantifier blow-up. No step reduces by the paper's own equations to a fitted parameter, self-defined quantity, or load-bearing self-citation; the derivation is self-contained against external model-checking results.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract-only review; no free parameters, axioms, or invented entities are specified in the provided text.

pith-pipeline@v0.9.0 · 5734 in / 1188 out tokens · 27365 ms · 2026-05-24T11:54:32.171556+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

113 extracted references · 113 canonical work pages

  1. [1]

    Faster pa- rameterized algorithms for minor containment

    Isolde Adler, Frederic Dorn, Fedor V Fomin, Ignasi Sau, a nd Dimitrios M Thilikos. Faster pa- rameterized algorithms for minor containment. Theoretical Computer Science, 412(50):7018– 7028, 2011

    work page 2011

  2. [2]

    Compu ting excluded minors

    Isolde Adler, Martin Grohe, and Stephan Kreutzer. Compu ting excluded minors. In Proc. of the 29th Annual ACM-SIAM Symposium on Discrete Algorithms ( SODA 2008) , pages 641–650. SIAM, 2008

    work page 2008

  3. [3]

    Kolliopoulos, Philipp Klaus Kr ause, Daniel Lokshtanov, Saket Saurabh, and Dimitrios M

    Isolde Adler, Stavros G. Kolliopoulos, Philipp Klaus Kr ause, Daniel Lokshtanov, Saket Saurabh, and Dimitrios M. Thilikos. Irrelevant vertices fo r the planar disjoint paths problem. J. Comb. Theory, Ser. B , 122:815–843, 2017

    work page 2017

  4. [4]

    On the width of regular classes of finite structures

    Alexsander Andrade de Melo and Mateus de Oliveira Olivei ra. On the width of regular classes of finite structures. In Proc. of the 27th International Conference on Automated Deduc tion (CADE 2019) , pages 18–34. Springer, 2019. 23

    work page 2019

  5. [5]

    Easy p roblems for tree-decomposable graphs

    Stefan Arnborg, Jens Lagergren, and Detlef Seese. Easy p roblems for tree-decomposable graphs. Journal of Algorithms , 12(2):308–340, 1991

    work page 1991

  6. [6]

    Positive-instance dr iven dynamic programming for graph searching

    Max Bannach and Sebastian Berndt. Positive-instance dr iven dynamic programming for graph searching. In Workshop on Algorithms and Data Structures , pages 43–56. Springer, 2019

    work page 2019

  7. [7]

    Practical access to dy namic programming on tree decompositions

    Max Bannach and Sebastian Berndt. Practical access to dy namic programming on tree decompositions. Algorithms, 12(8):172, 2019

    work page 2019

  8. [8]

    Fellows, Lars Jaffke, Tom´ aˇ s Masaˇ r ´ ık, Mateus de Oliveira Oliveira, Geevarghese Philip, and Frances A

    Julien Baste, Michael R. Fellows, Lars Jaffke, Tom´ aˇ s Masaˇ r ´ ık, Mateus de Oliveira Oliveira, Geevarghese Philip, and Frances A. Rosamond. Diversity of s olutions: An exploration through the lens of fixed-parameter tractability theory. Artificial Intelligence , 303:103644, 2022

    work page 2022

  9. [9]

    Thilikos

    Julien Baste, Ignasi Sau, and Dimitrios M. Thilikos. A co mplexity dichotomy for hitting connected minors on bounded treewidth graphs: the chair and the banner draw the boundary. In SODA, pages 951–970. SIAM, 2020

    work page 2020

  10. [10]

    On non-serial dynamic programming

    Umberto Bertele and Francesco Brioschi. On non-serial dynamic programming. J. Comb. Theory, Ser. A , 14(2):137–148, 1973

    work page 1973

  11. [11]

    Therese C. Biedl. On triangulating k-outerplanar grap hs. Discret. Appl. Math. , 181(1):275– 279, 2015

    work page 2015

  12. [12]

    A linear-time algorithm for finding t ree-decompositions of small treewidth

    Hans L Bodlaender. A linear-time algorithm for finding t ree-decompositions of small treewidth. SIAM Journal on computing , 25(6):1305–1317, 1996

    work page 1996

  13. [13]

    Treewidth: Algorithmic techniques and results

    Hans L Bodlaender. Treewidth: Algorithmic techniques and results. In Proc. of the 22nd International Symposium on Mathematical Foundations of Comp uter Science , pages 19–36. Springer, 1997

    work page 1997

  14. [14]

    A partial k-arboretum of graphs with bounded treewidth

    Hans L Bodlaender. A partial k-arboretum of graphs with bounded treewidth. Theoretical computer science, 209(1-2):1–45, 1998

    work page 1998

  15. [15]

    Deterministic single exponential time algorithms for connectivity probl ems parameterized by treewidth

    Hans L Bodlaender, Marek Cygan, Stefan Kratsch, and Jes per Nederlof. Deterministic single exponential time algorithms for connectivity probl ems parameterized by treewidth. Information and Computation , 243:86–111, 2015

    work page 2015

  16. [16]

    Combinatorial op timization on graphs of bounded treewidth

    Hans L Bodlaender and Arie MCA Koster. Combinatorial op timization on graphs of bounded treewidth. The Computer Journal , 51(3):255–269, 2008

    work page 2008

  17. [17]

    Bodlaender

    H.L. Bodlaender. Classes of graphs with bounded tree-w idth. Technical Report RUU-CS- 86-22, Department of Information and Computing Sciences, U trecht University, 1986

    work page 1986

  18. [18]

    Definability equals recognizability for graphs of bounded treewidth

    Miko/suppress laj Boja´ nczyk and Michal Pilipczuk. Definability equals recognizability for graphs of bounded treewidth. In Proc. of the 31st Annual ACM/IEEE Symposium on Logic in Com- puter Science (LICS 2016) , pages 407–416. ACM, 2016

    work page 2016

  19. [19]

    Cutwidth approximation in linear time

    HD Booth, Rajeev Govindan, Michael A Langston, and Sidd harthan Ramachandramurthi. Cutwidth approximation in linear time. In Proc. of the 2nd Great Lakes Symposium on VLSI, pages 70–73. IEEE, 1992

    work page 1992

  20. [20]

    Borie, R

    Richard B. Borie, R. Gary Parker, and Craig A. Tovey. Alg orithms for recognition of regular properties and decomposition of recursive graph families. Ann. Oper. Res. , 33(3):125–149, 1991. 24

    work page 1991

  21. [21]

    Graph classes: a survey

    Andreas Brandst¨ adt, Van Bang Le, and Jeremy P Spinrad. Graph classes: a survey . SIAM, 1999

    work page 1999

  22. [22]

    The complexity of satisfiability of small depth circuits

    Chris Calabro, Russell Impagliazzo, and Ramamohan Pat uri. The complexity of satisfiability of small depth circuits. In Proc. of the 4th International Workshop on Parameterized and Exact Computation , pages 75–85. Springer, 2009

    work page 2009

  23. [23]

    Carmosino, Jiawei Gao, Russell Impagliazzo, I van Mihajlin, Ramamohan Paturi, and Stefan Schneider

    Marco L. Carmosino, Jiawei Gao, Russell Impagliazzo, I van Mihajlin, Ramamohan Paturi, and Stefan Schneider. Nondeterministic extensions of the s trong exponential time hypothesis and consequences for non-reducibility. In Proc. of the 7th ACM Conference on Innovations in Theoretical Computer Science (ITCS 2016) , pages 261–270. ACM, 2016

    work page 2016

  24. [24]

    Graphs with small bandwi dth and cutwidth

    Fan RK Chung and Paul D Seymour. Graphs with small bandwi dth and cutwidth. Discrete Mathematics, 75(1-3):113–119, 1989

    work page 1989

  25. [25]

    Excluded grid theorem: Improved and sim plified

    Julia Chuzhoy. Excluded grid theorem: Improved and sim plified. In Proc. of the 47th annual ACM symposium on Theory of Computing , pages 645–654, 2015

    work page 2015

  26. [26]

    Improved bounds for the flat wall theorem

    Julia Chuzhoy. Improved bounds for the flat wall theorem . In Proc. of the 2015 ACM-SIAM Symposium on Discrete Algorithms , pages 256–275. SIAM, 2015

    work page 2015

  27. [27]

    Tree automata techniques and applications, 2008

    Hubert Comon, Max Dauchet, R´ emi Gilleron, Florent Jac quemard, Denis Lugiez, Christof L¨ oding, Sophie Tison, and Marc Tommasi. Tree automata techniques and applications, 2008

    work page 2008

  28. [28]

    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

    work page 1990

  29. [29]

    The monadic second-order logic of gra phs XV: On a conjecture by d

    Bruno Courcelle. The monadic second-order logic of gra phs XV: On a conjecture by d. Seese. Journal of Applied Logic , 4(1):79–114, 2006

    work page 2006

  30. [30]

    Computations by fly- automata beyond monadic second- order logic

    Bruno Courcelle and Ir` ene Durand. Computations by fly- automata beyond monadic second- order logic. Theor. Comput. Sci. , 619:32–67, 2016

    work page 2016

  31. [31]

    Graph structure and monadic second-order logic: A language-theoretic approach, volume 138

    Bruno Courcelle and Joost Engelfriet. Graph structure and monadic second-order logic: A language-theoretic approach, volume 138. Cambridge University Press, 2012

    work page 2012

  32. [32]

    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

    work page 2000

  33. [33]

    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

    work page 2015

  34. [34]

    Locall y excluding a minor

    Anuj Dawar, Martin Grohe, and Stephan Kreutzer. Locall y excluding a minor. In Proc. of the 22nd ACM/IEEE Anual Symposium on Logic in Computer Science ( LICS 2007) , pages 270–279. IEEE Computer Society, 2007

    work page 2007

  35. [35]

    An algorithmic metatheor em for directed treewidth

    Mateus de Oliveira Oliveira. An algorithmic metatheor em for directed treewidth. Discrete Applied Mathematics , 204:49–76, 2016

    work page 2016

  36. [36]

    Rodney G Downey and Michael R. Fellows. Parameterized complexity. Springer Science & Business Media, 2012

    work page 2012

  37. [37]

    Context-free graph properties via definable decompositions

    Michael Elberfeld. Context-free graph properties via definable decompositions. In Proc. of the 25th Conference on Computer Science Logic (CSL 2016) , volume 62 of LIPIcs, pages 17:1–17:16, 2016. 25

    work page 2016

  38. [38]

    Tutte’s 3-flow conjecture and short cycle covers

    GH Fan. Tutte’s 3-flow conjecture and short cycle covers . Journal of Combinatorial Theory, Series B , 57(1):36–43, 1993

    work page 1993

  39. [39]

    Query evalu ation via tree-decompositions

    J¨ org Flum, Markus Frick, and Martin Grohe. Query evalu ation via tree-decompositions. Journal of the ACM (JACM) , 49(6):716–752, 2002

    work page 2002

  40. [40]

    D ynamic programming as graph searching: An algebraic approach

    Stefania Gnesi, Ugo Montanari, and Alberto Martelli. D ynamic programming as graph searching: An algebraic approach. Journal of the ACM (JACM) , 28(4):737–751, 1981

    work page 1981

  41. [41]

    ¨Uber eine klassifikation der streckenkomplexe

    Hugo Hadwiger. ¨Uber eine klassifikation der streckenkomplexe. Vierteljschr. Naturforsch. Ges. Z¨ urich, 88(2):133–142, 1943

    work page 1943

  42. [42]

    S-functions for graphs

    Rudolf Halin. S-functions for graphs. Journal of geometry , 8(1-2):171–186, 1976

    work page 1976

  43. [43]

    Branch decompositions and minor contain ment

    Illya V Hicks. Branch decompositions and minor contain ment. Networks: An International Journal, 43(1):1–9, 2004

    work page 2004

  44. [44]

    Branch–width and tangles

    Illya V Hicks, Sang-il Oum, James J Cochran, Louis A Cox, Pinar Keskinocak, Jeffrey P Kharoufeh, and J Cole Smith. Branch–width and tangles. Wiley Encyclopedia of Operations Research and Management Science , 2010

    work page 2010

  45. [45]

    On the compl exity of k-SAT

    Russell Impagliazzo and Ramamohan Paturi. On the compl exity of k-SAT. J. Comput. Syst. Sci., 62(2):367–375, 2001

    work page 2001

  46. [46]

    Which problems have strongly exponential complexity? J

    Russell Impagliazzo, Ramamohan Paturi, and Francis Za ne. Which problems have strongly exponential complexity? J. Comput. Syst. Sci. , 63(4):512–530, 2001

    work page 2001

  47. [47]

    Determining the smallest k such that g is k -outerplanar

    Frank Kammer. Determining the smallest k such that g is k -outerplanar. In European Symposium on Algorithms , pages 359–370. Springer, 2007

    work page 2007

  48. [48]

    Algorit hms for finding an induced cycle in planar graphs

    Ken-ichi Kawarabayashi and Yusuke Kobayashi. Algorit hms for finding an induced cycle in planar graphs. Comb., 30(6):715–734, 2010

    work page 2010

  49. [49]

    Some recent pr ogress and applications in graph minor theory

    Ken-ichi Kawarabayashi and Bojan Mohar. Some recent pr ogress and applications in graph minor theory. Graphs Comb. , 23(1):1–46, 2007

    work page 2007

  50. [50]

    Ken-ichi Kawarabayashi, Bojan Mohar, and Bruce A. Reed . A simpler linear time algorithm for embedding graphs into an arbitrary surface and the genus of graphs of bounded tree- width. In FOCS, pages 771–780. IEEE Computer Society, 2008

    work page 2008

  51. [51]

    Hadwiger’s con jecture is decidable

    Ken-ichi Kawarabayashi and Bruce Reed. Hadwiger’s con jecture is decidable. In Proc. of the 41st Annual ACM Symposium on Theory of Computing , pages 445–454, 2009

    work page 2009

  52. [52]

    A new proof of the flat wall theorem

    Ken-ichi Kawarabayashi, Robin Thomas, and Paul Wollan . A new proof of the flat wall theorem. Journal of Combinatorial Theory, Series B , 129:204–238, 2018

    work page 2018

  53. [53]

    Thilikos

    Eun Jung Kim, Sang-il Oum, Christophe Paul, Ignasi Sau, and Dimitrios M. Thilikos. An FPT 2-approximation for tree-cut decomposition. Algorithmica, 80(1):116–135, 2018

    work page 2018

  54. [54]

    Tree-width, path-width, and cutwidth

    Ephraim Korach and Nir Solel. Tree-width, path-width, and cutwidth. Discrete Applied Mathematics, 43(1):97–101, 1993

    work page 1993

  55. [55]

    A single-exponential time 2-approxi mation algorithm for treewidth

    Tuukka Korhonen. A single-exponential time 2-approxi mation algorithm for treewidth. In Proc. of the 62nd Annual Symposium on Foundations of Computer Science (FOCS 2022) , pages 184–192. IEEE, 2022

    work page 2022

  56. [56]

    The cdp: A unifying formu lation for heuristic search, dynamic programming, and branch-and-bound

    Vipin Kumar and Laveen N Kanal. The cdp: A unifying formu lation for heuristic search, dynamic programming, and branch-and-bound. In Search in Artificial Intelligence , pages 1–27. Springer, 1988. 26

    work page 1988

  57. [57]

    Tools for tree sear ches: Dynamic programming

    C Le´ on, G Miranda, and C Rodr ´ ıguez. Tools for tree sear ches: Dynamic programming. Optimization Techniques for Solving Complex Problems , pages 209–230, 2009

    work page 2009

  58. [58]

    Lower bounds based on the exponential time hypothesis

    Daniel Lokshtanov, D´ aniel Marx, and Saket Saurabh. Lower bounds based on the exponential time hypothesis. Bull. EATCS , 105:41–72, 2011

    work page 2011

  59. [59]

    Mouawad, Saket Saurabh, and Meirav Zehavi

    Daniel Lokshtanov, Amer E. Mouawad, Saket Saurabh, and Meirav Zehavi. Packing cycles faster than erdos-posa. SIAM J. Discret. Math. , 33(3):1194–1215, 2019

    work page 2019

  60. [60]

    Roda, I Coloma, and A Del- gado

    D Gonzalez Morales, Francisco Almeida, C Rodrıguez, Jo se L. Roda, I Coloma, and A Del- gado. Parallel dynamic programming and automata theory. Parallel computing , 26(1):113– 134, 2000

    work page 2000

  61. [61]

    Jesper Nederlof, Michal Pilipczuk, C´ eline M. F. Swennenhuis, and Karol Wegrzycki. Isolation schemes for problems on decomposable graphs. In STACS, volume 219 of LIPIcs, pages 50:1– 50:20. Schloss Dagstuhl - Leibniz-Zentrum f¨ ur Informatik, 2022

    work page 2022

  62. [62]

    Subgraphs satisfying MSO properties on z-topologically order- able digraphs

    Mateus de Oliveira Oliveira. Subgraphs satisfying MSO properties on z-topologically order- able digraphs. In International Symposium on Parameterized and Exact Computat ion, pages 123–136. Springer, 2013

    work page 2013

  63. [63]

    Approximating clique-wi dth and branch-width

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

    work page 2006

  64. [64]

    A utomata theory meets ap- proximate dynamic programming: Optimal control with tempo ral logic constraints

    Ivan Papusha, Jie Fu, Ufuk Topcu, and Richard M Murray. A utomata theory meets ap- proximate dynamic programming: Optimal control with tempo ral logic constraints. In Proc. of the 55th IEEE Conference on Decision and Control (CDC 2016) , pages 434–440. IEEE, 2016

    work page 2016

  65. [65]

    Automata- based parsing in dynamic programming for linear indexed gra mmars

    Miguel Angel Alonso Pardo, Eric De La Clergerie, and Man uel Vilares Ferro. Automata- based parsing in dynamic programming for linear indexed gra mmars. Proc. of DIALOGUE , 97:22–27, 1997

    work page 1997

  66. [66]

    Partial order programming

    D Stott Parker. Partial order programming. In Proceedings of the 16th ACM SIGPLAN- SIGACT symposium on Principles of programming languages , pages 260–266, 1989

    work page 1989

  67. [67]

    Problems parameterized by treewidth tractable in single exponential time: A logical approach

    Micha/suppress l Pilipczuk. Problems parameterized by treewidth tractable in single exponential time: A logical approach. In Proc. of the 36th International Symposium on Mathematical Fo unda- tions of Computer Science , pages 520–531. Springer, 2011

    work page 2011

  68. [68]

    Recent techniques and results on the erd˝ os–p´ osa property.Discrete Applied Mathematics , 231:25–43, 2017

    Jean-Florent Raymond and Dimitrios M Thilikos. Recent techniques and results on the erd˝ os–p´ osa property.Discrete Applied Mathematics , 231:25–43, 2017

    work page 2017

  69. [69]

    Hadwig er’s conjecture fork 6-free graphs

    Neil Robertson, Paul Seymour, and Robin Thomas. Hadwig er’s conjecture fork 6-free graphs. Combinatorica, 13(3):279–361, 1993

    work page 1993

  70. [70]

    Graph minors

    Neil Robertson and Paul D Seymour. Graph minors. III. Pl anar tree-width. Journal of Combinatorial Theory, Series B , 36(1):49–64, 1984

    work page 1984

  71. [71]

    Graph minors

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

    work page 1986

  72. [72]

    A more accurate view of the flat wall theorem

    Ignasi Sau, Giannos Stamoulis, and Dimitrios M Thiliko s. A more accurate view of the flat wall theorem. arXiv preprint arXiv:2102.06463 , 2021

    work page arXiv 2021

  73. [73]

    The structure of the models of decidable m onadic theories of graphs

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

    work page 1991

  74. [74]

    Hadwiger’s conjecture

    Paul Seymour. Hadwiger’s conjecture. Springer, 2016

    work page 2016

  75. [75]

    Cutwidth I: A linear time fixed parameter algorithm

    Dimitrios M Thilikos, Maria Serna, and Hans L Bodlaende r. Cutwidth I: A linear time fixed parameter algorithm. Journal of Algorithms , 56(1):1–24, 2005

    work page 2005

  76. [76]

    Constructive linear time algo- rithms for small cutwidth and carving-width

    Dimitrios M Thilikos, Maria J Serna, and Hans L Bodlaend er. Constructive linear time algo- rithms for small cutwidth and carving-width. In Proc. of the 11th International Symposium on Algorithms and Computation , pages 192–203. Springer, 2000

    work page 2000

  77. [77]

    A contribution to the theory of ch romatic polynomials

    William Thomas Tutte. A contribution to the theory of ch romatic polynomials. Canadian journal of mathematics , 6:80–91, 1954

    work page 1954

  78. [78]

    Recent progress in combinatoric s

    William Thomas Tutte. Recent progress in combinatoric s. In Proceedings of the 3rd Waterloo Conference on Combinatorics . Academic Press, 1969

    work page 1969

  79. [79]

    Johan M. M. van Rooij, Hans L. Bodlaender, and Peter Ross manith. Dynamic programming on tree decompositions using generalised fast subset convo lution. In ESA, volume 5757 of Lecture Notes in Computer Science , pages 566–577. Springer, 2009

    work page 2009

  80. [80]

    Nowher e-zero 4-flow in almost petersen-minor free graphs

    Xiaofeng Wang, Cun-Quan Zhang, and Taoye Zhang. Nowher e-zero 4-flow in almost petersen-minor free graphs. Discrete mathematics, 309(5):1025–1032, 2009

    work page 2009

Showing first 80 references.