Documentation

Complexity.Foundations.Combinatorics.DepthReduction

Valiant's depth reduction #

A grading of a set E of edges with D levels is a labelling of the vertices by numbers below D that increases along every edge (IsGrading). The levels increase along every path, so a path of edges of E has at most D vertices; labelling every vertex of a directed acyclic graph by the number of vertices on a longest path ending at it is a grading, so this is a way of bounding the depth of the graph. Valiant's depth reduction [Val77], Jukna, Lemma 1.4: if E has a grading with 2 ^ k levels, then for every r ≤ k, removing some r / k of the edges leaves edges with a grading with 2 ^ (k - r) levels (IsGrading.exists_sdiff).

An edge (u, v) is in class b when the levels of u and v first differ, from the top, at bit b (InClass). Each edge is in at most one class, so among k classes one has at most 1 / k of the edges; deleting bit b from every level grades all edges outside class b with half the levels. Repeating r times removes at most r / k of the edges.

Main definitions #

Main results #

References #

source
def Cslib.IsGrading {V : Type u_1} (E : Finset (V × V)) (D : ℕ) (g : V → ℕ) :
Prop

g grades the edges E with D levels: its values are below D, and it increases along every edge.

Instances For
    source
    theorem Cslib.IsGrading.mono {V : Type u_1} {E F : Finset (V × V)} {D : ℕ} {g : V → ℕ} (hg : IsGrading E D g) (hF : F ⊆ E) :
    IsGrading F D g

    A grading of the edges E grades every subset F ⊆ E.

    source
    theorem Cslib.IsGrading.exists_sdiff {V : Type u_1} {E : Finset (V × V)} {g : V → ℕ} [DecidableEq V] {k r : ℕ} (hg : IsGrading E (2 ^ k) g) (hr : r ≤ k) :
    ∃ F ⊆ E, k * F.card ≤ r * E.card ∧ ∃ (g' : V → ℕ), IsGrading (E \ F) (2 ^ (k - r)) g'

    Valiant's depth reduction. If E has a grading with 2 ^ k levels and r ≤ k, then removing at most r / k of the edges leaves edges with a grading with 2 ^ (k - r) levels.