On Algorithmic Certification of Graph Structures

On Algorithmic Certification of Graph Structures Oliver Bachtler Department of Mathematics RPTU in Kaiserslautern 30.03.2023 Motivation Four Colour Theorem (informal version) Every map can be coloured with at most four colours. Four Colour Theorem Every planar graph is 4-colourable. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 1 / 25 Motivation Four Colour Theorem (informal version) Every map can be coloured with at most four colours. Four Colour Theorem Every planar graph is 4-colourable. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 1 / 25 Motivation Four Colour Theorem (informal version) Every map can be coloured with at most four colours. Four Colour Theorem Every planar graph is 4-colourable. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 1 / 25 Motivation Four Colour Theorem (informal version) Every map can be coloured with at most four colours. Four Colour Theorem Every planar graph is 4-colourable. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 1 / 25 Motivation Four Colour Theorem (informal version) Every map can be coloured with at most four colours. Four Colour Theorem Every planar graph is 4-colourable. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 1 / 25 Motivation Four Colour Theorem (informal version) Every map can be coloured with at most four colours. Four Colour Theorem Every planar graph is 4-colourable. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 1 / 25 Proving the Four Colour Theorem Find a set of configurations that is ▶reducible and ▶checked by a computer ▶unavoidable. ▶by hand, 400 pages Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 2 / 25 Proving the Four Colour Theorem Find a set of configurations that is ▶reducible and ▶checked by a computer ▶unavoidable. ▶by hand, 400 pages Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 2 / 25 Proving the Four Colour Theorem Find a set of configurations that is ▶reducible and ▶checked by a computer ▶unavoidable. ▶by hand, 400 pages Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 2 / 25 Proving the Four Colour Theorem Find a set of configurations that is ▶reducible and ▶checked by a computer ▶unavoidable. ▶by hand, 400 pages Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 2 / 25 Proving the Four Colour Theorem Find a set of configurations that is ▶reducible and ▶checked by a computer ▶unavoidable. ▶by hand, 400 pages Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 2 / 25 Outline The 3-Decomposition Conjecture Introduction Reducible Configurations Unavoidable Structures Automation For Unavoidable Structures Obtaining an Algorithm Speeding It Up Does It Even Terminate Thesis Overview Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 3 / 25 The 3-Decomposition Conjecture Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 4 / 25 3-Decompositions of Graphs Definition A graph is cubic if every vertex has degree 3. Definition A3-decomposition of a connected cubic graph Gconsists of ▶aspanning tree T, ▶aunion of cycles C, and ▶amatching M such that E(G)is the disjoint union E(T)∪E(C)∪M. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 5 / 25 3-Decompositions of Graphs Definition A graph is cubic if every vertex has degree 3. Definition A3-decomposition of a connected cubic graph Gconsists of ▶aspanning tree T, ▶aunion of cycles C, and ▶amatching M such that E(G)is the disjoint union E(T)∪E(C)∪M. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 5 / 25 3-Decompositions of Graphs Definition A graph is cubic if every vertex has degree 3. Definition A3-decomposition of a connected cubic graph Gconsists of ▶aspanning tree T, ▶aunion of cycles C, and ▶amatching M such that E(G)is the disjoint union E(T)∪E(C)∪M. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 5 / 25 An Example Graph ▶Given: connected cubic graph. ▶Take a spanning tree. ▶The remaining edges form cycles and paths. ▶Want paths of length 1. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 6 / 25 An Example Graph ▶Given: connected cubic graph. ▶Take a spanning tree. ▶The remaining edges form cycles and paths. ▶Want paths of length 1. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 6 / 25 The 3-Decomposition Conjecture Definition A3-decomposition of a connected cubic graph Gconsists of ▶aspanning tree T, ▶aunion of cycles C, and ▶amatching M such that E(G)is the disjoint union E(T)∪E(C)∪M. 3-Decomposition Conjecture Every connected cubic graph has a 3-decomposition. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 7 / 25 Literature Overview ▶Hamiltonian ▶traceable ▶3-conn. planar, projective plane ▶‘3 cycles’ ▶‘cacti-ish’ ▶‘star-like’ ▶3-connected Torus, Klein Bottle ▶planar ▶claw-free ▶3-connected tree-width 3 ▶3-connected path-width 4 2011 2015 2016 2018 2019 2020 2021 2022 [Hof11] [AJS15] [Abd+16] [LL20] [Bot+21] [BK22] [OY16] [XZZ20] [Cam11] [Bac15] [HKO18] [Hei19] [HLY20] [BH21] [AAA18] Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 8 / 25 Literature Overview ▶Hamiltonian ▶traceable ▶3-conn. planar, projective plane ▶‘3 cycles’ ▶‘cacti-ish’ ▶‘star-like’ ▶3-connected Torus, Klein Bottle ▶planar ▶claw-free ▶3-connected tree-width 3 ▶3-connected path-width 4 2011 2015 2016 2018 2019 2020 2021 2022 [Hof11] [AJS15] [Abd+16] [LL20] [Bot+21] [BK22] [OY16] [XZZ20] [Cam11] [Bac15] [HKO18] [Hei19] [HLY20] [BH21] [AAA18] Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 8 / 25 Literature Overview ▶Hamiltonian ▶traceable ▶3-conn. planar, projective plane ▶‘3 cycles’ ▶‘cacti-ish’ ▶‘star-like’ ▶3-connected Torus, Klein Bottle ▶planar ▶claw-free ▶3-connected tree-width 3 ▶3-connected path-width 4 2011 2015 2016 2018 2019 2020 2021 2022 [Hof11] [AJS15] [Abd+16] [LL20] [Bot+21] [BK22] [OY16] [XZZ20] [Cam11] [Bac15] [HKO18] [Hei19] [HLY20] [BH21] [AAA18] Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 8 / 25 Literature Overview ▶Hamiltonian ▶traceable ▶3-conn. planar, projective plane ▶‘3 cycles’ ▶‘cacti-ish’ ▶‘star-like’ ▶3-connected Torus, Klein Bottle ▶planar ▶claw-free ▶3-connected tree-width 3 ▶3-connected path-width 4 2011 2015 2016 2018 2019 2020 2021 2022 [Hof11] [AJS15] [Abd+16] [LL20] [Bot+21] [BK22] [OY16] [XZZ20] [Cam11] [Bac15] [HKO18] [Hei19] [HLY20] [BH21] [AAA18] Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 8 / 25 Literature Overview ▶Hamiltonian ▶traceable ▶3-conn. planar, projective plane ▶‘3 cycles’ ▶‘cacti-ish’ ▶‘star-like’ ▶3-connected Torus, Klein Bottle ▶planar ▶claw-free ▶3-connected tree-width 3 ▶3-connected path-width 4 2011 2015 2016 2018 2019 2020 2021 2022 [Hof11] [AJS15] [Abd+16] [LL20] [Bot+21] [BK22] [OY16] [XZZ20] [Cam11] [Bac15] [HKO18] [Hei19] [HLY20] [BH21] [AAA18] Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 8 / 25 Literature Overview ▶Hamiltonian ▶traceable ▶3-conn. planar, projective plane ▶‘3 cycles’ ▶‘cacti-ish’ ▶‘star-like’ ▶3-connected Torus, Klein Bottle ▶planar ▶claw-free ▶3-connected tree-width 3 ▶3-connected path-width 4 2011 2015 2016 2018 2019 2020 2021 2022 [Hof11] [AJS15] [Abd+16] [LL20] [Bot+21] [BK22] [OY16] [XZZ20] [Cam11] [Bac15] [HKO18] [Hei19] [HLY20] [BH21] [AAA18] Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 8 / 25 Literature Overview ▶Hamiltonian ▶traceable ▶3-conn. planar, projective plane ▶‘3 cycles’ ▶‘cacti-ish’ ▶‘star-like’ ▶3-connected Torus, Klein Bottle ▶planar ▶claw-free ▶3-connected tree-width 3 ▶3-connected path-width 4 2011 2015 2016 2018 2019 2020 2021 2022 [Hof11] [AJS15] [Abd+16] [LL20] [Bot+21] [BK22] [OY16] [XZZ20] [Cam11] [Bac15] [HKO18] [Hei19] [HLY20] [BH21] [AAA18] Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 8 / 25 Literature Overview ▶Hamiltonian ▶traceable ▶3-conn. planar, projective plane ▶‘3 cycles’ ▶‘cacti-ish’ ▶‘star-like’ ▶3-connected Torus, Klein Bottle ▶planar ▶claw-free ▶3-connected tree-width 3 ▶3-connected path-width 4 2011 2015 2016 2018 2019 2020 2021 2022 [Hof11] [AJS15] [Abd+16] [LL20] [Bot+21] [BK22] [OY16] [XZZ20] [Cam11] [Bac15] [HKO18] [Hei19] [HLY20] [BH21] [AAA18] Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 8 / 25 Literature Overview ▶Hamiltonian ▶traceable ▶3-conn. planar, projective plane ▶‘3 cycles’ ▶‘cacti-ish’ ▶‘star-like’ ▶3-connected Torus, Klein Bottle ▶planar ▶claw-free ▶3-connected tree-width 3 ▶3-connected path-width 4 2011 2015 2016 2018 2019 2020 2021 2022 [Hof11] [AJS15] [Abd+16] [LL20] [Bot+21] [BK22] [OY16] [XZZ20] [Cam11] [Bac15] [HKO18] [Hei19] [HLY20] [BH21] [AAA18] Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 8 / 25 Reducible Configurations Definition Areducible configuration is a graph that is not part of a (3-connected) minimum counterexample to the 3-decomposition conjecture. Example The triangle is reducible. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 9 / 25 Reducible Configurations Definition Areducible configuration is a graph that is not part of a (3-connected) minimum counterexample to the 3-decomposition conjecture. Example The triangle is reducible. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 9 / 25 Reducible Configurations Definition Areducible configuration is a graph that is not part of a (3-connected) minimum counterexample to the 3-decomposition conjecture. Example The triangle is reducible. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 9 / 25 Reducible Configurations Definition Areducible configuration is a graph that is not part of a (3-connected) minimum counterexample to the 3-decomposition conjecture. Example The triangle is reducible. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 9 / 25 A Bigger Example Example The claw-square is reducible. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 10 / 25 A Bigger Example Example The claw-square is reducible. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 10 / 25 A List of Reducible Configurations Theorem The graphs below are reducible configurations. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 11 / 25 Unavoidable Structures Question: Are these reducible configurations unavoidable? Answer: No (sadly). Solution: Restrict the class of cubic graphs to make them unavoidable. ⇒Bound the path-width. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 12 / 25 Unavoidable Structures Question: Are these reducible configurations unavoidable? Answer: No (sadly). Solution: Restrict the class of cubic graphs to make them unavoidable. ⇒Bound the path-width. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 12 / 25 Unavoidable Structures Question: Are these reducible configurations unavoidable? Answer: No (sadly). Solution: Restrict the class of cubic graphs to make them unavoidable. ⇒Bound the path-width. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 12 / 25 Bounding the Path-Width Theorem Cubic graphs of path-width at most 4contain a reducible configuration. Corollary Every (3-connected) cubic graph of path-width at most 4satisfies the 3-decomposition conjecture. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 14 / 25 Bounding the Path-Width Theorem Cubic graphs of path-width at most 4contain a reducible configuration. Corollary Every (3-connected) cubic graph of path-width at most 4satisfies the 3-decomposition conjecture. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 14 / 25 Automation For Unavoidable Structures Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 15 / 25 Finding Unavoidable Structures for Bounded Path-Width 3-Decomposition Conjecture Every connected cubic graph has a 3-decomposition. Four Colour Theorem Every planar graph is 4-colourable. Conjecture Every graph in Gsatisfies property π. Question: Does every graph in Gof path-width at most kcontain a subgraph in U? Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 16 / 25 Finding Unavoidable Structures for Bounded Path-Width 3-Decomposition Conjecture Every connected cubic graph has a 3-decomposition. Four Colour Theorem Every planar graph is 4-colourable. Conjecture Every graph in Gsatisfies property π. Question: Does every graph in Gof path-width at most kcontain a subgraph in U? Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 16 / 25 Finding Unavoidable Structures for Bounded Path-Width 3-Decomposition Conjecture Every connected cubic graph has a 3-decomposition. Four Colour Theorem Every planar graph is 4-colourable. Conjecture Every graph in Gsatisfies property π. Question: Does every graph in Gof path-width at most kcontain a subgraph in U? Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 16 / 25 Finding Unavoidable Structures for Bounded Path-Width 3-Decomposition Conjecture Every connected cubic graph has a 3-decomposition. Four Colour Theorem Every planar graph is 4-colourable. Conjecture Every graph in Gsatisfies property π. Question: Does every graph in Gof path-width at most kcontain a subgraph in U? Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 16 / 25 Finding Unavoidable Structures for Bounded Path-Width 3-Decomposition Conjecture Every connected cubic graph has a 3-decomposition. Four Colour Theorem Every planar graph is 4-colourable. Conjecture Every cubic graph satisfies property π. Question: Does every cubic graph of path-width at most kcontain a subgraph in U? Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 16 / 25 Answering the Question Q: Does every cubic graph of path-width at most 3contain a ? Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 17 / 25 Answering the Question Q: Does every cubic graph of path-width at most 3contain a ? Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 17 / 25 Answering the Question Q: Does every cubic graph of path-width at most 3contain a ? Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 17 / 25 Answering the Question Q: Does every cubic graph of path-width at most 3contain a ? Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 17 / 25 Answering the Question Q: Does every cubic graph of path-width at most 3contain a ? Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 17 / 25 Answering the Question Q: Does every cubic graph of path-width at most 3contain a ? Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 17 / 25 Answering the Question Q: Does every cubic graph of path-width at most 3contain a ? Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 17 / 25 Answering the Question Q: Does every cubic graph of path-width at most 3contain a ? Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 17 / 25 Answering the Question Q: Does every cubic graph of path-width at most 3contain a ? Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 17 / 25 Answering the Question Q: Does every cubic graph of path-width at most 3contain a ? Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 17 / 25 Answering the Question Q: Does every cubic graph of path-width at most 3contain a ? A: No! Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 17 / 25 Answering the Question Q: Does every cubic graph of path-width at most 3contain a or a ∆? Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 17 / 25 Developing an Algorithm def FindStructures(U,k): Initialise a queue Qwith Ek+1 while Q=∅do G←Q.dequeue() foreach vibrant vertex u∈Gdo foreach choice of edges Fat udo G′←G+F+v,uis dulled if G′contains a subgraph in Uthen continue if G′yields a counterexample Hthen return H Q.append(G′) Q=G ′ = Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 18 / 25 Developing an Algorithm def FindStructures(U,k): Initialise a queue Qwith Ek+1 while Q=∅do G←Q.dequeue() foreach vibrant vertex u∈Gdo foreach choice of edges Fat udo G′←G+F+v,uis dulled if G′contains a subgraph in Uthen continue if G′yields a counterexample Hthen return H Q.append(G′) Q=G ′ = u Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 18 / 25 Developing an Algorithm def FindStructures(U,k): Initialise a queue Qwith Ek+1 while Q=∅do G←Q.dequeue() foreach vibrant vertex u∈Gdo foreach choice of edges Fat udo G′←G+F+v,uis dulled if G′contains a subgraph in Uthen continue if G′yields a counterexample Hthen return H Q.append(G′) Q=G ′ = u F Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 18 / 25 Developing an Algorithm def FindStructures(U,k): Initialise a queue Qwith Ek+1 while Q=∅do G←Q.dequeue() foreach vibrant vertex u∈Gdo foreach choice of edges Fat udo G′←G+F+v,uis dulled if G′contains a subgraph in Uthen continue if G′yields a counterexample Hthen return H Q.append(G′) Q=G ′ = u F Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 18 / 25 Developing an Algorithm def FindStructures(U,k): Initialise a queue Qwith Ek+1 while Q=∅do G←Q.dequeue() foreach vibrant vertex u∈Gdo foreach choice of edges Fat udo G′←G+F+v,uis dulled if G′contains a subgraph in Uthen continue if G′yields a counterexample Hthen return H Q.append(G′) Q=G ′ = Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 18 / 25 Developing an Algorithm def FindStructures(U,k): Initialise a queue Qwith Ek+1 while Q=∅do G←Q.dequeue() foreach vibrant vertex u∈Gdo foreach choice of edges Fat udo G′←G+F+v,uis dulled if G′contains a subgraph in Uthen continue if G′yields a counterexample Hthen return H Q.append(G′) Q=G ′ = Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 18 / 25 Developing an Algorithm def FindStructures(U,k): Initialise a queue Qwith Ek+1 while Q=∅do G←Q.dequeue() foreach vibrant vertex u∈Gdo foreach choice of edges Fat udo G′←G+F+v,uis dulled if G′contains a subgraph in Uthen continue if G′yields a counterexample Hthen return H Q.append(G′) Q=G′= Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 18 / 25 Developing an Algorithm def FindStructures(U,k): Initialise a queue Qwith Ek+1 while Q=∅do G←Q.dequeue() foreach vibrant vertex u∈Gdo foreach choice of edges Fat udo G′←G+F+v,uis dulled if G′contains a subgraph in Uthen continue if G′yields a counterexample Hthen return H Q.append(G′) Q=G′= Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 18 / 25 Developing an Algorithm def FindStructures(U,k): Initialise a queue Qwith Ek+1 while Q=∅do G←Q.dequeue() foreach vibrant vertex u∈Gdo foreach choice of edges Fat udo G′←G+F+v,uis dulled if G′contains a subgraph in Uthen continue if G′yields a counterexample Hthen return H Q.append(G′) Q=G′= Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 18 / 25 Developing an Algorithm def FindStructures(U,k): Initialise a queue Qwith Ek+1 while Q=∅do G←Q.dequeue() foreach vibrant vertex u∈Gdo foreach choice of edges Fat udo G′←G+F+v,uis dulled if G′contains a subgraph in Uthen continue if G′yields a counterexample Hthen return H Q.append(G′) Q= G ′ = Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 18 / 25 How Slow Is This Actually? Example: 5 graphs. Algorithm: 45 graphs. x4 Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 19 / 25 How Slow Is This Actually? Example: 5 graphs. Algorithm: 45 graphs. x4 Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 19 / 25 How Slow Is This Actually? Example: 5 graphs. Algorithm: 45 graphs. x4 Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 19 / 25 How Slow Is This Actually? Example: 5 graphs. Algorithm: 45 graphs. x4 Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 19 / 25 How Slow Is This Actually? Example: 5 graphs. Algorithm: 45 graphs. x4 Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 19 / 25 Teaching the Algorithm to Recognise Symmetries Definition Avibrant automorphism φof a graph Gis ▶an automorphism φ ▶that maps 7→ and 7→ Using vibrant automorphisms ▶foreach vibrant vertex u∈Gdo ▶foreach choice of edges Fat udo x4 Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 20 / 25 Teaching the Algorithm to Recognise Symmetries Definition Avibrant automorphism φof a graph Gis ▶an automorphism φ ▶that maps 7→ and 7→ Using vibrant automorphisms ▶foreach vibrant vertex u∈Gdo ▶foreach choice of edges Fat udo x4 Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 20 / 25 Teaching the Algorithm to Recognise Symmetries Definition Avibrant automorphism φof a graph Gis ▶an automorphism φ ▶that maps 7→ and 7→ Using vibrant automorphisms ▶foreach vibrant vertex u∈Gdo ▶foreach choice of edges Fat udo x4 Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 20 / 25 Teaching the Algorithm to Recognise Symmetries Definition Avibrant automorphism φof a graph Gis ▶an automorphism φ ▶that maps 7→ and 7→ Using vibrant automorphisms ▶foreach vibrant vertex u∈Gdo ▶foreach choice of edges Fat udo x4 Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 20 / 25 Teaching the Algorithm to Recognise Symmetries Definition Avibrant automorphism φof a graph Gis ▶an automorphism φ ▶that maps 7→ and 7→ Using vibrant automorphisms ▶foreach vibrant vertex u∈Gdo ▶foreach choice of edges Fat udo x4 Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 20 / 25 Teaching the Algorithm to Recognise Symmetries Definition Avibrant automorphism φof a graph Gis ▶an automorphism φ ▶that maps 7→ and 7→ Using vibrant automorphisms ▶foreach vibrant vertex u∈Gdo ▶foreach choice of edges Fat udo x4 Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 20 / 25 Teaching the Algorithm to Recognise Symmetries Definition Avibrant automorphism φof a graph Gis ▶an automorphism φ ▶that maps 7→ and 7→ Using vibrant automorphisms ▶foreach vibrant vertex u∈Gdo ▶foreach choice of edges Fat udo x4 Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 20 / 25 Teaching the Algorithm to Recognise Symmetries Definition Avibrant automorphism φof a graph Gis ▶an automorphism φ ▶that maps 7→ and 7→ Using vibrant automorphisms ▶foreach vibrant vertex u∈Gdo ▶foreach choice of edges Fat udo x4 Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 20 / 25 Does It Even Terminate? ▶If a counterexample exists, then the algorithm finds (a smallest) one. ▶Otherwise, we might be in trouble. For example, let Gcontain the following graphs: We can construct these as follows: The triangle appears arbitrarily late! Lemma ([BH20]) In general, determining whether Uis unavoidable for Gis undecidable. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 21 / 25 Does It Even Terminate? ▶If a counterexample exists, then the algorithm finds (a smallest) one. ▶Otherwise, we might be in trouble. For example, let Gcontain the following graphs: We can construct these as follows: The triangle appears arbitrarily late! Lemma ([BH20]) In general, determining whether Uis unavoidable for Gis undecidable. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 21 / 25 Does It Even Terminate? ▶If a counterexample exists, then the algorithm finds (a smallest) one. ▶Otherwise, we might be in trouble. For example, let Gcontain the following graphs: We can construct these as follows: The triangle appears arbitrarily late! Lemma ([BH20]) In general, determining whether Uis unavoidable for Gis undecidable. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 21 / 25 Does It Even Terminate? ▶If a counterexample exists, then the algorithm finds (a smallest) one. ▶Otherwise, we might be in trouble. For example, let Gcontain the following graphs: We can construct these as follows: The triangle appears arbitrarily late! Lemma ([BH20]) In general, determining whether Uis unavoidable for Gis undecidable. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 21 / 25 Does It Even Terminate? ▶If a counterexample exists, then the algorithm finds (a smallest) one. ▶Otherwise, we might be in trouble. For example, let Gcontain the following graphs: We can construct these as follows: The triangle appears arbitrarily late! Lemma ([BH20]) In general, determining whether Uis unavoidable for Gis undecidable. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 21 / 25 Does It Even Terminate? ▶If a counterexample exists, then the algorithm finds (a smallest) one. ▶Otherwise, we might be in trouble. For example, let Gcontain the following graphs: We can construct these as follows: The triangle appears arbitrarily late! Lemma ([BH20]) In general, determining whether Uis unavoidable for Gis undecidable. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 21 / 25 Does It Even Terminate? ▶If a counterexample exists, then the algorithm finds (a smallest) one. ▶Otherwise, we might be in trouble. For example, let Gcontain the following graphs: We can construct these as follows: The triangle appears arbitrarily late! Lemma ([BH20]) In general, determining whether Uis unavoidable for Gis undecidable. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 21 / 25 Does It Even Terminate? ▶If a counterexample exists, then the algorithm finds (a smallest) one. ▶Otherwise, we might be in trouble. For example, let Gcontain the following graphs: We can construct these as follows: The triangle appears arbitrarily late! Lemma ([BH20]) In general, determining whether Uis unavoidable for Gis undecidable. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 21 / 25 Does It Even Terminate? ▶If a counterexample exists, then the algorithm finds (a smallest) one. ▶Otherwise, we might be in trouble. For example, let Gcontain the following graphs: We can construct these as follows: The triangle appears arbitrarily late! Lemma ([BH20]) In general, determining whether Uis unavoidable for Gis undecidable. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 21 / 25 Does It Even Terminate? ▶If a counterexample exists, then the algorithm finds (a smallest) one. ▶Otherwise, we might be in trouble. For example, let Gcontain the following graphs: We can construct these as follows: The triangle appears arbitrarily late! Lemma ([BH20]) In general, determining whether Uis unavoidable for Gis undecidable. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 21 / 25 Does It Even Terminate? ▶If a counterexample exists, then the algorithm finds (a smallest) one. ▶Otherwise, we might be in trouble. For example, let Gcontain the following graphs: We can construct these as follows: The triangle appears arbitrarily late! Lemma ([BH20]) In general, determining whether Uis unavoidable for Gis undecidable. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 21 / 25 Does It Even Terminate? ▶If a counterexample exists, then the algorithm finds (a smallest) one. ▶Otherwise, we might be in trouble. For example, let Gcontain the following graphs: We can construct these as follows: The triangle appears arbitrarily late! Lemma ([BH20]) In general, determining whether Uis unavoidable for Gis undecidable. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 21 / 25 Does It Even Terminate? ▶If a counterexample exists, then the algorithm finds (a smallest) one. ▶Otherwise, we might be in trouble. For example, let Gcontain the following graphs: We can construct these as follows: The triangle appears arbitrarily late! Lemma ([BH20]) In general, determining whether Uis unavoidable for Gis undecidable. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 21 / 25 Does It Even Terminate? ▶If a counterexample exists, then the algorithm finds (a smallest) one. ▶Otherwise, we might be in trouble. For example, let Gcontain the following graphs: We can construct these as follows: The triangle appears arbitrarily late! Lemma ([BH20]) In general, determining whether Uis unavoidable for Gis undecidable. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 21 / 25 Does It Even Terminate? ▶If a counterexample exists, then the algorithm finds (a smallest) one. ▶Otherwise, we might be in trouble. For example, let Gcontain the following graphs: We can construct these as follows: The triangle appears arbitrarily late! Lemma ([BH20]) In general, determining whether Uis unavoidable for Gis undecidable. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 21 / 25 Does It Even Terminate? ▶If a counterexample exists, then the algorithm finds (a smallest) one. ▶Otherwise, we might be in trouble. For example, let Gcontain the following graphs: We can construct these as follows: The triangle appears arbitrarily late! Lemma ([BH20]) In general, determining whether Uis unavoidable for Gis undecidable. Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 21 / 25 The Good News Theorem ([BH20]) The algorithm can be modified such that it terminates for the cubic case if Uis a finite set of connected graphs. Idea ▶Discard more graphs. ▶Take care that not all counterexamples are lost. This is small! Oliver Bachtler Algorithmic Certification of Graph Structures 30.03.2023 22 / 25