arxiv: 2605.11025 · v1 · submitted 2026-05-10 · 💻 cs.DS · cs.CC· cs.LO· math.CO

Recognition: 2 theorem links

· Lean Theorem

State Canonization and Early Pruning in Width-Based Automated Theorem Proving

Mateus de Oliveira Oliveira , Sam Urmian

Authors on Pith no claims yet

Pith reviewed 2026-05-13 01:32 UTC · model grok-4.3

classification 💻 cs.DS cs.CCcs.LOmath.CO

keywords width-based automated theorem provingstate canonizationearly pruningReed's conjecturetreewidthpathwidthtriangle-free graphsdynamic programming

0 comments

The pith

State canonization and early pruning allow automated verification that Reed's conjecture holds for triangle-free graphs of pathwidth at most 5.

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

The paper advances width-based automated theorem proving by adding two practical reductions to dynamic programming searches on tree decompositions. State canonization eliminates redundant states during the search for counterexamples, while early pruning discards branches early when testing implications between properties where one is closed under subgraphs. Applied to Reed's conjecture on triangle-free graphs, the method proves the conjecture holds on all such graphs of pathwidth at most 5 and treewidth at most 3. It also automatically produces counterexamples to several invalid strengthenings of the conjecture. These results are the first concrete evidence that the framework can handle real graph-theoretic questions on bounded-width classes.

Core claim

By combining dynamic programming algorithms on tree decompositions with state canonization that reduces evaluated states and early pruning applicable to implications P1 implies P2 where P1 is subgraph-closed, the search becomes efficient enough to confirm Reed's conjecture for triangle-free graphs on pathwidth at most 5 and treewidth at most 3 while constructing counterexamples to invalid strengthenings.

What carries the argument

State-canonization technique that reduces the number of states in the dynamic-programming search, paired with early-pruning that discards subtrees for subgraph-closed antecedent properties.

If this is right

The same techniques can test additional long-standing graph conjectures on all graphs of small pathwidth or treewidth.
Automated counterexample generation becomes feasible for invalid strengthenings of other conjectures of the form P1 implies P2.
Practical running times are achieved for k up to 5 even though the theoretical bound remains doubly exponential.
The framework can now be applied directly to study coloring properties restricted to triangle-free graphs of bounded width.

Where Pith is reading between the lines

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

Similar canonization maps may be definable for other width measures such as branchwidth or clique-width.
Early pruning could be extended to properties closed under minors or other operations beyond subgraphs.
The approach suggests that hybrid human-automated workflows could first use the method to rule out small-width counterexamples before attempting manual proofs.

Load-bearing premise

The canonization and pruning steps preserve both soundness and completeness of the original dynamic-programming search over tree decompositions.

What would settle it

Discovery of a triangle-free graph of pathwidth 5 that violates Reed's conjecture, or failure to recover known counterexamples to the tested strengthenings.

Figures

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

**Figure 2.** Figure 2: A triangle-free graph with 22 vertices, pathwidth 4, chromatic number 4, and max [PITH_FULL_IMAGE:figures/full_fig_p036_2.png] view at source ↗

read the original abstract

Width-based automated theorem proving is a framework where counterexamples to graph-theoretic conjectures are searched width-wise relative to some graph width measure, such as treewidth or pathwidth. In a recent work it has been shown that dynamic programming algorithms operating on tree decompositions can be combined together with the purpose of width-based theorem proving. This approach can be used to show that several long-standing conjectures in graph theory can be tested in time \(2^{2^{k^{O(1)}}}\) on the class of graphs of treewidth at most \(k\). In this work, we give the first steps towards evaluating the viability of this framework from a practical standpoint. At the same time, we advance the framework in two directions. First, we introduce a state-canonization technique that significantly reduces the number of states evaluated during the search for a counterexample of the conjecture. Second, we introduce an early-pruning technique that can be applied in the study of conjectures of the form \(\mathcal{P}_1 \rightarrow \mathcal{P}_2\), for graph properties \(\mathcal{P}_1\) and \(\mathcal{P}_2\), where \(\mathcal{P}_1\) is a property closed under subgraphs. As a concrete application, we use our framework in the study of graph-theoretic conjectures related to coloring triangle-free graphs. In particular, our algorithm is able to show that Reed's conjecture for triangle-free graphs is valid on the class of graphs of pathwidth at most 5, and on graphs of treewidth at most 3. Perhaps more interestingly, our algorithm is able to construct in a completely automated way counterexamples to invalid strengthenings of Reed's conjecture. These are the first results showing that width-based automated theorem proving is a promising avenue in the study of graph-theoretic conjectures.

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.

Desk Editor's Note private letter to a colleague

The paper adds state canonization and early pruning to the width-based DP framework and uses them to verify Reed's conjecture on triangle-free graphs up to pathwidth 5 and treewidth 3 while generating automated counterexamples to some strengthenings, but the soundness of those reductions is the part that still needs verification.

read the letter

The main takeaway is that this work moves the width-based automated theorem proving idea from a theoretical double-exponential bound toward something that can actually run on small widths. The authors introduce state canonization to collapse equivalent states during the DP search and an early-pruning rule that applies when the conjecture has the form P1 implies P2 with P1 closed under subgraphs. They then apply the resulting procedure to Reed's conjecture restricted to triangle-free graphs and report that it holds for all such graphs of pathwidth at most 5 and treewidth at most 3. They also produce counterexamples to several invalid strengthenings in a fully automated way. These are the first concrete negative results coming out of the framework rather than just positive verifications. The prior work was mainly about composing existing DP routines on tree decompositions; the new reductions and the counterexample outputs are the actual advance here. The paper does a reasonable job showing that the method can be implemented and that it produces usable output on a known conjecture. That alone makes the practical viability claim more credible than before. The soft spot is the one flagged in the stress test. Canonization and pruning are presented as safe optimizations, but the letter does not include an explicit argument or small-case check that they never discard a reachable counterexample state or accept an invalid one. Because the approach composes DP transitions from the earlier paper, any mismatch in how the reduced states interact with the acceptance conditions or the width-k decompositions would break the exhaustive guarantee. The abstract gives no state counts, pruning statistics, or runtime figures, so the full text needs to supply enough detail for a reader to confirm the reductions are faithful. This paper is aimed at people working on automated methods for graph conjectures or on practical dynamic programming over decompositions. A reader who wants to test similar coloring or structural conjectures on bounded-width graphs will find the techniques and the specific Reed results worth looking at. It deserves peer review because the results are new and the optimizations address a real bottleneck, even if the soundness argument will probably need tightening during revision.

Referee Report

2 major / 1 minor

Summary. The paper advances width-based automated theorem proving by introducing state-canonization to reduce evaluated states and early-pruning for conjectures of the form P1 → P2 where P1 is subgraph-closed. It applies the framework to Reed's conjecture on triangle-free graphs, claiming to verify validity on all graphs of pathwidth at most 5 and treewidth at most 3, while also automatically constructing counterexamples to certain invalid strengthenings.

Significance. If the canonization and pruning steps are shown to preserve soundness and completeness of the underlying DP on tree decompositions, the results would be significant as the first concrete, automated verification and counterexample generation for a long-standing graph conjecture within this framework, moving beyond the theoretical 2^{2^{k^{O(1)}}} bound to practical feasibility.

major comments (2)

[Abstract] Abstract: the headline claims that the algorithm verifies Reed's conjecture on pathwidth ≤5 and treewidth ≤3, and constructs counterexamples to invalid strengthenings, rest on the assertion that state-canonization and early-pruning preserve the exhaustive-search guarantee of the composed DP routines; no correctness argument, machine-checked proof, or enumeration of edge cases for the reductions is referenced, making the central results unverifiable from the given information.
[Abstract (early-pruning description)] The early-pruning technique for subgraph-closed P1 is presented as safe, yet the manuscript must demonstrate that no reachable counterexample state is ever pruned and that acceptance conditions remain unchanged; without an explicit invariant or proof that the reduced state space still captures all counterexamples to P1 → P2, the completeness claim for the reported counterexamples is load-bearing and unestablished.

minor comments (1)

[Abstract] The abstract mentions combining DP algorithms from prior work but does not clarify how the new reductions interact with the specific tree-decomposition routines or state representations used for coloring properties.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the detailed and constructive report. The concerns about establishing the correctness of state-canonization and early-pruning are valid and central to the claims. We will revise the manuscript to include explicit proofs, invariants, and edge-case analysis.

read point-by-point responses

Referee: [Abstract] Abstract: the headline claims that the algorithm verifies Reed's conjecture on pathwidth ≤5 and treewidth ≤3, and constructs counterexamples to invalid strengthenings, rest on the assertion that state-canonization and early-pruning preserve the exhaustive-search guarantee of the composed DP routines; no correctness argument, machine-checked proof, or enumeration of edge cases for the reductions is referenced, making the central results unverifiable from the given information.

Authors: We agree that the current manuscript does not reference or provide a formal correctness argument, machine-checked proof, or enumeration of edge cases. We will add a dedicated subsection proving that state-canonization (via selection of canonical representatives) and the overall composition preserve the exhaustive-search property of the underlying DP. The revision will include a manual proof of soundness and completeness together with enumeration of key edge cases (e.g., empty graphs, single vertices, and boundary states on tree decompositions). We will not add a machine-checked proof in this revision. revision: yes
Referee: [Abstract (early-pruning description)] The early-pruning technique for subgraph-closed P1 is presented as safe, yet the manuscript must demonstrate that no reachable counterexample state is ever pruned and that acceptance conditions remain unchanged; without an explicit invariant or proof that the reduced state space still captures all counterexamples to P1 → P2, the completeness claim for the reported counterexamples is load-bearing and unestablished.

Authors: We accept the point. The current version lacks an explicit invariant or proof for early-pruning. In the revision we will introduce a formal invariant showing that pruning never discards a state from which a counterexample to P1 → P2 is reachable, and we will prove that acceptance conditions are unchanged. The argument relies on the subgraph-closed nature of P1 to guarantee that any counterexample has a minimal witness that survives pruning. This will be placed in the new correctness subsection and will directly support the completeness claim for the automatically generated counterexamples. revision: yes

Circularity Check

0 steps flagged

Minor self-citation to prior DP framework; new canonization/pruning techniques asserted independent

full rationale

The paper cites a recent work for the base dynamic-programming framework combining algorithms on tree decompositions. The new state-canonization and early-pruning techniques are introduced as practical reductions whose soundness/completeness is claimed to hold independently of the target conjecture (Reed's). No equations, definitions, or fitted parameters in the abstract or described results reduce the reported outcomes (validity on pathwidth ≤5/treewidth ≤3, automated counterexamples) to inputs by construction. The self-citation is present but not load-bearing for the central claims, which rest on the new reductions applied to the framework. This is a normal minor self-citation case with independent content.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract-only review; no explicit free parameters, axioms, or invented entities are described. The underlying dynamic-programming framework is treated as given from prior literature.

pith-pipeline@v0.9.0 · 5641 in / 1382 out tokens · 47989 ms · 2026-05-13T01:32:34.307404+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/AlexanderDuality.lean (D=3 forcing via circle linking) alexander_duality_circle_linking unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

our algorithm is able to show that Reed's conjecture for triangle-free graphs is valid on the class of graphs of pathwidth at most 5, and on graphs of treewidth at most 3... counterexamples to invalid strengthenings
IndisputableMonolith/Cost/FunctionalEquation.lean (J-cost uniqueness) washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

state-canonization technique... early-pruning technique... (k,D)-refutation... CAN_k_D(b,S)

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

68 extracted references · 68 canonical work pages

[1]

TreeWidzard: A tool for width-based automated theorem proving

AutoProving Project. TreeWidzard: A tool for width-based automated theorem proving. https://github.com/AutoProving/TreeWidzard-Engine, 2026. Software repository

work page 2026
[2]

Structure-guided automated reasoning.arXiv preprint arXiv:2312.14620, 2023

Max Bannach and Markus Hecher. Structure-guided automated reasoning.arXiv preprint arXiv:2312.14620, 2023

work page arXiv 2023
[3]

Clark Barrett, Christopher L Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovi´ c, Tim King, Andrew Reynolds, and Cesare Tinelli. CVC4. InInternational Conference on Computer Aided Verification, pages 171–177. Springer, 2011

work page 2011
[4]

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

work page 2015
[5]

Bodlaender.Classes of graphs with bounded tree-width

Hans L. Bodlaender.Classes of graphs with bounded tree-width. PhD thesis, Utrecht University, 1986

work page 1986
[6]

Dynamic programming on graphs with bounded treewidth

Hans L Bodlaender. Dynamic programming on graphs with bounded treewidth. InInter- national Colloquium on Automata, Languages, and Programming, pages 105–118. Springer, 1988

work page 1988
[7]

Equitable colorings of bounded treewidth graphs

Hans L Bodlaender and Fedor V Fomin. Equitable colorings of bounded treewidth graphs. Theoretical Computer Science, 349(1):22–30, 2005

work page 2005
[8]

Combinatorial optimization on graphs of bounded treewidth.The Computer Journal, 51(3):255–269, 2008

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

work page 2008
[9]

Hadwiger’s conjecture is true for almost every graph.Eur

B´ ela Bollob´ as, Paul A Catlin, and Paul Erd¨ os. Hadwiger’s conjecture is true for almost every graph.Eur. J. Comb., 1(3):195–199, 1980

work page 1980
[10]

SIAM, 1999

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

work page 1999
[11]

R. L. Brooks. On colouring the nodes of a network.Mathematical Proceedings of the Cambridge Philosophical Society, 37(2):194–197, 1941. 41

work page 1941
[12]

On dominating sets of maximal outerplanar graphs

CN Campos and Yoshiko Wakabayashi. On dominating sets of maximal outerplanar graphs. Discrete Applied Mathematics, 161(3):330–335, 2013

work page 2013
[13]

The monadic second-order logic of graphs

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

work page 1990
[14]

Automata for the verification of monadic second-order graph properties.Journal of applied logic, 10(4):368–409, 2012

Bruno Courcelle and Ir` ene Durand. Automata for the verification of monadic second-order graph properties.Journal of applied logic, 10(4):368–409, 2012

work page 2012
[15]

Z3: An efficient SMT solver

Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. InInternational conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 337–340. Springer, 2008

work page 2008
[16]

From width-based model checking to width- based automated theorem proving

Mateus de Oliveira Oliveira and Farhad Vadiee. From width-based model checking to width- based automated theorem proving. InProceedings of the AAAI Conference on Artificial Intelligence, volume 37, pages 6297–6304, 2023

work page 2023
[17]

Triangle-free graphs of tree-width t are⌈(t+ 3)/ 2⌉-colorable.European Journal of Combinatorics, 66:95–100, 2017

Zdenˇ ek Dvoˇ r´ ak and Ken-ichi Kawarabayashi. Triangle-free graphs of tree-width t are⌈(t+ 3)/ 2⌉-colorable.European Journal of Combinatorics, 66:95–100, 2017

work page 2017
[18]

Answer set solv- ing with bounded treewidth revisited

Johannes K Fichte, Markus Hecher, Michael Morak, and Stefan Woltran. Answer set solv- ing with bounded treewidth revisited. InInternational Conference on Logic Programming and Nonmonotonic Reasoning, pages 132–145. Springer, 2017

work page 2017
[19]

Theory solving made easy with clingo 5

Martin Gebser, Roland Kaminski, Benjamin Kaufmann, Max Ostrowski, Torsten Schaub, and Philipp Wanko. Theory solving made easy with clingo 5. InTechnical Communications of the 32nd International Conference on Logic Programming (ICLP 2016), volume 52 of OpenAccess Series in Informatics (OASIcs), pages 2:1–2:15. Schloss Dagstuhl–Leibniz- Zentrum f¨ ur Inform...

work page 2016
[20]

Game chromatic number of outerplanar graphs.Journal of Graph Theory, 30(1):67–70, 1999

DJ Guan and Xuding Zhu. Game chromatic number of outerplanar graphs.Journal of Graph Theory, 30(1):67–70, 1999

work page 1999
[21]

On the bend-number of planar and outerplanar graphs.Discrete Applied Mathematics, 179:109–119, 2014

Daniel Heldt, Kolja Knauer, and Torsten Ueckerdt. On the bend-number of planar and outerplanar graphs.Discrete Applied Mathematics, 179:109–119, 2014

work page 2014
[22]

The circular chromatic number of series-parallel graphs

Pavol Hell and Xuding Zhu. The circular chromatic number of series-parallel graphs. Journal of Graph Theory, 33(1):14–24, 2000

work page 2000
[23]

Is the five-flow conjecture almost false?Journal of Combinatorial Theory, Series B, 103(4):532–565, 2013

Jesper Lykke Jacobsen and Jes´ us Salas. Is the five-flow conjecture almost false?Journal of Combinatorial Theory, Series B, 103(4):532–565, 2013

work page 2013
[24]

Determining the smallest k such that g is k-outerplanar

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

work page 2007
[25]

Springer, 1994

Ton Kloks.Treewidth: computations and approximations. Springer, 1994

work page 1994
[26]

First-order theorem proving and Vampire

Laura Kov´ acs and Andrei Voronkov. First-order theorem proving and Vampire. InInter- national Conference on Computer Aided Verification, pages 1–35. Springer, 2013

work page 2013
[27]

Tight relation between the circular chromatic number and the girth of series-parallel graphs.Discrete mathematics, 254(1-3):393–404, 2002

Zhishi Pan and Xuding Zhu. Tight relation between the circular chromatic number and the girth of series-parallel graphs.Discrete mathematics, 254(1-3):393–404, 2002

work page 2002
[28]

Tutte’s 3-flow conjecture for almost even graphs

L´ eo Vieira Peres and Ricardo Dahab. Tutte’s 3-flow conjecture for almost even graphs. Procedia Computer Science, 195:280–288, 2021. 42

work page 2021
[29]

Oriented vertex and arc colorings of outerplanar graphs

Alexandre Pinlou and ´Eric Sopena. Oriented vertex and arc colorings of outerplanar graphs. Information Processing Letters, 100(3):97–104, 2006

work page 2006
[30]

From bandwidthkto pathwidthk

Andrzej Proskurowski and Jan Arne Telle. From bandwidthkto pathwidthk. InPro- ceedings of the 5th Italian Conference on Theoretical Computer Science (ICTCS’98), pages 90–101. World Scientific, 1998

work page 1998
[31]

Bruce Reed.ω,δ, andχ.Journal of Graph Theory, 27(4):177–212, 1998

work page 1998
[32]

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

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

work page 1991
[33]

SPASS version 3.5

Christoph Weidenbach, Dilyana Dimova, Arnaud Fietzke, Rohit Kumar, Martin Suda, and Patrick Wischnewski. SPASS version 3.5. InAutomated Deduction–CADE-22: 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings 22, pages 140–145. Springer, 2009

work page 2009
[34]

Upper bounds for the zagreb indices and the spectral radius of series-parallel graphs.International Journal of Quantum Chemistry, 107(4):875–878, 2007

Bo Zhou. Upper bounds for the zagreb indices and the spectral radius of series-parallel graphs.International Journal of Quantum Chemistry, 107(4):875–878, 2007. 43 Summary of Notation Symbol Meaning Nnatural numbers{0,1,2, . . .} N+ positive natural numbersN\ {0} [n]{1, . . . , n}(with [0] =∅) Pfin(X),P(X) finite subsets / all subsets ofX G= (V(G), E(G), ...

work page 2007
[35]

The mapsϕ 1 :V(G 1)→V(G)andν 1 :E(G 1)→E(G)defined byϕ 1(v) ˙ = 2vand ν1(e) ˙ = 2eform an embedding ofG 1 intoG

work page
[36]

Moreover, for eachu∈B(τ)we haveϕ 1(θ[σ1](u)) =ϕ 2(θ[σ2](u)) =θ[τ](u)

The mapsϕ 2 :V(G 2)→V(G)andν 2 :E(G 2)→E(G)defined byϕ 2(v) ˙ =µ(2v+ 1)and ν2(e) ˙ = 2e+ 1form an embedding ofG 2 intoG. Moreover, for eachu∈B(τ)we haveϕ 1(θ[σ1](u)) =ϕ 2(θ[σ2](u)) =θ[τ](u). Proof.LetH˙ =G 1 ⊎G 2 be the disjoint union. By the disjoint union construction (Section 2), the left copyG (0) 1 uses even vertex/edge identifiers and the right copy...

work page
[37]

Ifw̸=band{u, v}⊈dom(w), return∅

work page
[38]

If eitherw(u) =d−1 orw(v) =d−1, return{b}

work page
[39]

Otherwise, return {(w|dom(w)\{u,v}∪{u→w(u) + 1, v→w(v) + 1})}. Join. Letwandw ′ be local witnesses associated with the left and right children of a given node, respectively. The goal of theJoinoperation is to merge the graphs corresponding to these children along the vertices labeled with active labels. 49 The process begins by checking whether either chi...

work page
[40]

Ifw=borw ′ =b, return{b}

work page
[41]

Ifdom(w)̸=dom(w ′), return∅

work page
[42]

If there existsu∈dom(w) such thatw(u) +w ′(u)≥d, return{b}

work page
[43]

potential clique,

Otherwise, return{w ′′}, where for eachu∈dom(w),w ′′(u) =w(u) +w ′(u). Final Witness Function.The final witness function is used to determine whether the con- dition of finding a vertex with a degree of at leastdhas been satisfied. This function checks ifw=b. Ifw=b, it confirms that a vertex with the required degree has been found, and the function output...

work page
[45]

Ifw= (γ, s) andu∈dom(γ), then return∅

work page
[46]

Ifw= (γ, s),u /∈dom(γ), ands=ω, then return{w}

work page
[47]

Ifw= (γ, s),u /∈dom(γ),s < ω, ands=|dom(γ)|, then return {(γ, s),(γ∪ {u→0}, s+ 1)}

work page
[48]

Forget Vertex

Ifw= (γ, s),u /∈dom(γ),s < ω, ands >|dom(γ)|, then return{(γ, s)}. Forget Vertex. Letwbe aSimpleCliqueNumber AtLeast(ω)[k]-local witness, and letu represent a label in [k+ 1]. When the vertex labeleduis forgotten, the labeluis freed, making it available for reuse when introducing a future vertex. The behavior of this function depends on the current state ...

work page
[49]

Ifw=b, then return{w}

work page
[50]

Ifw= (γ, s) andu /∈dom(γ), then return{(γ, s)}

work page
[51]

Ifw= (γ, s),u∈dom(γ), ands < ω, then return∅

work page
[52]

Ifw= (γ, ω),u∈dom(γ), andγ(u)̸=ω−1, then return∅

work page
[53]

Introduce Edge

Ifw= (γ, ω),u∈dom(γ), andγ(u) =ω−1, then return {(γ|dom(γ)\{u}, ω)}. Introduce Edge. Letwbe a local witness, and suppose a new edge is introduced between two distinct labeled verticesuandv. This operation updates the local witnesswto reflect the addition of the new edge, with the behavior depending on the current state ofw. Ifw=b, then the local witness i...

work page
[54]

If eitheruorvis not indom(γ), return{w}

work page
[55]

Ifu, v∈dom(γ) and eitherγ(u) =ω−1 orγ(v) =ω−1, return∅

work page
[56]

Letwandw ′ be local witnesses associated with the left and right children of a given node, respectively

Ifu, v∈dom(γ), create a new map γ′ =γ| dom(γ)\{u,v} ∪{u→γ(u) + 1, v→γ(v) + 1} •Ifs=ωand for alll∈dom(γ ′),γ ′(l) =ω−1 return {b} •otherwise, return {(γ′, s)} Join. Letwandw ′ be local witnesses associated with the left and right children of a given node, respectively. The goal of theJoinoperation is to merge the graphs corresponding to these children alon...

work page
[57]

If eitherw=borw ′ =b, return{b}

work page
[58]

If|dom(γ)|< sand|dom(γ ′)|< s ′, return∅

work page
[59]

Ifdom(γ)̸=dom(γ ′), return∅

work page
[60]

If there existsu∈dom(γ) such thatγ(u) +γ ′(u)> ω−1, return∅

work page
[61]

Otherwise, createγ ′′ where for allu∈dom(γ) 2,γ ′′(u) =γ(u) +γ ′(u), and lets ′′ = s+s ′ − |dom(γ)|. •Ifs ′′ =ωand for allu∈dom(γ ′′),γ ′′(u) =ω−1, return {b} •Otherwise return {(γ′′, s′′)} Final Witness Function.The final witness function checks if the local witnesswhas success- fully found a clique of sizeω. Ifw=b, meaning a clique of the required size ...

work page
[62]

Ifw=b, the setSforms a clique of sizeω

work page
[63]

(a)|S|=s, (b)S∩θ[τ](B(τ)) =θ[τ](dom(γ)), and (c) for eachu∈dom(γ), we haveγ(u) =d G(τ)[S] (θ[τ](u)), and for eachx∈S\ θ[τ](dom(γ)),d G(τ)[S] (x) =ω−1

Ifw= (γ, s), then the following conditions are satisfied. (a)|S|=s, (b)S∩θ[τ](B(τ)) =θ[τ](dom(γ)), and (c) for eachu∈dom(γ), we haveγ(u) =d G(τ)[S] (θ[τ](u)), and for eachx∈S\ θ[τ](dom(γ)),d G(τ)[S] (x) =ω−1. (d)s < ωor there existsu∈dom(γ)such thatγ(u)< ω−1. The first condition indicates that ifw=b, then there should be a vertex setSthat forms a clique o...

work page
[64]

In particular, if the dynamization containsb, then the specified cleaning function makes the cleaned witness set equal to{b}

Ifb/∈Γ[SimpleCliqueNumber AtLeast(ω), k](τ), then for every map witnessw= (γ, s), w∈Γ[SimpleCliqueNumber AtLeast(ω), k](τ) if and only if Pred SimpleCliqueNumber AtLeast(ω, k)(τ,w) = 1. In particular, if the dynamization containsb, then the specified cleaning function makes the cleaned witness set equal to{b}. Proof.First ignore the cleaning function and ...

work page
[65]

If multiple edges have already been found (w= b), the local witness remains unchanged

work page
[66]

Ifw̸= b and the new edge creates a multiple edge (i.e.,{u, v} ∈w), then the returned local witness is the Boolean flag b

work page
[67]

HasMultipleEdges[k].IntroEdge{u, v}(w) =    {b}ifw= b, {w∪ {{u, v}}}ifw̸= b and{u, v}/∈w, {b}ifw̸= b and{u, v} ∈w

Otherwise, if{u, v}/∈w, the edge pair{u, v}is added tow. HasMultipleEdges[k].IntroEdge{u, v}(w) =    {b}ifw= b, {w∪ {{u, v}}}ifw̸= b and{u, v}/∈w, {b}ifw̸= b and{u, v} ∈w. Join.Letwandw ′ be local witnesses associated with the left and right children of a given node. The purpose of theJoinoperation is to combine the graphs corresponding to these chil...

work page
[68]

Ifw= b,G(τ)is a multigraph

work page
[69]

The first condition requires that if the witness is the Boolean flag b, the graph associated withτshould have multiple edges

Ifw̸= b,G(τ)is a simple graph and w= n {u, v} ∈ P(B(τ),2) :∃e∈E(G(τ))withendpts(e) ={θ[τ](u), θ[τ](v)} o . The first condition requires that if the witness is the Boolean flag b, the graph associated withτshould have multiple edges. The second condition ensures that if the witness is a set of label pairs, the graph is simple andwencodesexactlythose edges ...

work page