Compressions of multigraphs

Laying out a multigraph of bounded degree reduces to laying out a smaller multigraph, its quotient by a compression. Fix a budget d, at least the maximum degree. Partition the vertices into blocks, each listing its vertices in order, starting from single vertices. Two distinct blocks joined by an edge may be merged when at most d edges leave their union; the merged block lists the longer block first. A Compression records the invariants of this process:

• at most d edges leave a block;
• at most d log₂ |B| edges leave a proper prefix of a block B. A proper prefix of a merged block is a proper prefix of its first part, or all of its first part followed by a proper prefix of its second part, which has at most half as many vertices;
• there are at least as many blocks and edges inside blocks as vertices, since a merge loses one block and moves at least one edge inside.

Each merge loses a block, so merging ends in a saturated compression, to which no merge applies (Compression.exists_saturated).

The quotient of a compression is the multigraph whose vertices are the blocks and whose edges are the edges of the original multigraph between distinct blocks. By the counting invariant its cycle rank is at most that of the original multigraph (Compression.card_add_card_external_le). A layout of the quotient expands to a layout of the original multigraph, block by block and each block in its own order; the frontiers of the expanded layout exceed those of the layout of the quotient by at most d log₂ |V| edges (Compression.exists_width_le).

Main definitions

• Cslib.Circuits.Frontier.Multigraph.Compression: a partition into ordered blocks, with the invariants of merging.
• Cslib.Circuits.Frontier.Multigraph.Compression.Saturated: no merge applies.
• Cslib.Circuits.Frontier.Multigraph.Compression.quotient: the multigraph on the blocks.

Main results

• Cslib.Circuits.Frontier.Multigraph.Compression.exists_saturated: merging terminates.
• Cslib.Circuits.Frontier.Multigraph.Compression.ncard_edgeCut_preimage: the cut of a union of whole blocks is the cut of the quotient.
• Cslib.Circuits.Frontier.Multigraph.Compression.card_add_card_external_le: the cycle rank of the quotient is at most that of the multigraph.
• Cslib.Circuits.Frontier.Multigraph.Compression.exists_width_le: expanding a layout of the quotient.

structure Cslib.Circuits.Frontier.Multigraph.Compression {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (d : ℕ) : Type u_1

A compression of G with budget d: a partition of its vertices into blocks, each listing its vertices in order, with the invariants maintained by merging. A block B is identified with its vertex set {v | v ∈ B}.

• blocks : Finset (List V)

  The blocks.

• exists_mem (v : V) : ∃ B ∈ self.blocks, v ∈ B

  Every vertex lies in a block.

• eq_of_mem (B : List V) : B ∈ self.blocks → ∀ B' ∈ self.blocks, ∀ v ∈ B, v ∈ B' → B = B'

  Blocks sharing a vertex are equal.

• nodup (B : List V) : B ∈ self.blocks → B.Nodup

  A block lists each of its vertices once.

• ne_nil (B : List V) : B ∈ self.blocks → B ≠ []

  Blocks are nonempty.

• ncard_edgeCut_le (B : List V) : B ∈ self.blocks → (G.edgeCut {v : V | v ∈ B}).ncard ≤ d

  At most d edges leave a block.

• ncard_edgeCut_take_le (B : List V) : B ∈ self.blocks → ∀ k < B.length, (G.edgeCut {v : V | v ∈ List.take k B}).ncard ≤ d * Nat.log 2 B.length

  At most d log₂ |B| edges leave a proper prefix of a block B.

• card_le : Nat.card V ≤ self.blocks.card + {e : E | ∃ B ∈ self.blocks, G.src e ∈ B ∧ G.tgt e ∈ B}.ncard

  There are at least as many blocks and edges inside blocks as vertices.

Merging

def Cslib.Circuits.Frontier.Multigraph.Compression.singletons {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} [Fintype V] [DecidableEq V] [Finite E] (hG : G.MaxDegreeLE d) : G.Compression d

The compression into single vertices.

theorem Cslib.Circuits.Frontier.Multigraph.Compression.exists_merge {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) [Finite E] {B B' : List V} (hB : B ∈ c.blocks) (hB' : B' ∈ c.blocks) (hne : B ≠ B') (hjoin : (G.edgeCut {v : V | v ∈ B} ∩ G.edgeCut {v : V | v ∈ B'}).Nonempty) (hcut : (G.edgeCut ({v : V | v ∈ B} ∪ {v : V | v ∈ B'})).ncard ≤ d) : ∃ (c' : G.Compression d), c'.blocks.card < c.blocks.card

Merging. Two distinct blocks joined by an edge, with at most d edges leaving their union, may be replaced by their union, listing the longer block first.

def Cslib.Circuits.Frontier.Multigraph.Compression.Saturated {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) : Prop

A compression is saturated when no merge applies: more than d edges leave the union of any two distinct blocks joined by an edge.

theorem Cslib.Circuits.Frontier.Multigraph.Compression.exists_saturated {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} [Finite V] [Finite E] (hG : G.MaxDegreeLE d) : ∃ (c : G.Compression d), c.Saturated

Merging terminates. Every finite multigraph of maximum degree d has a saturated compression with budget d: one with the fewest blocks.

The quotient

noncomputable def Cslib.Circuits.Frontier.Multigraph.Compression.blockOf {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) (v : V) : ↥c.blocks

The block containing a vertex.

theorem Cslib.Circuits.Frontier.Multigraph.Compression.mem_blockOf {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) (v : V) : v ∈ ↑(c.blockOf v)

theorem Cslib.Circuits.Frontier.Multigraph.Compression.mem_iff_blockOf_eq {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) {v : V} {B : ↥c.blocks} : v ∈ ↑B ↔ c.blockOf v = B

theorem Cslib.Circuits.Frontier.Multigraph.Compression.preimage_blockOf_singleton {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) (B : ↥c.blocks) : c.blockOf ⁻¹' {B} = {v : V | v ∈ ↑B}

The vertices of a block are those it contains.

theorem Cslib.Circuits.Frontier.Multigraph.Compression.disjoint_of_ne {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) {B B' : ↥c.blocks} (h : B ≠ B') : Disjoint {v : V | v ∈ ↑B} {v : V | v ∈ ↑B'}

Distinct blocks are disjoint.

theorem Cslib.Circuits.Frontier.Multigraph.Compression.mem_edgeCut_block {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) {B : ↥c.blocks} {e : E} : e ∈ G.edgeCut {v : V | v ∈ ↑B} ↔ ¬(c.blockOf (G.src e) = B ↔ c.blockOf (G.tgt e) = B)

theorem Cslib.Circuits.Frontier.Multigraph.Compression.exists_ne_mem_edgeCut {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) {B : ↥c.blocks} {e : E} (he : e ∈ G.edgeCut {v : V | v ∈ ↑B}) : ∃ (B' : ↥c.blocks), B' ≠ B ∧ e ∈ G.edgeCut {v : V | v ∈ ↑B'}

An edge leaving a block leaves another block too.

theorem Cslib.Circuits.Frontier.Multigraph.Compression.edgeCut_nonempty {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) (hG : G.toSimpleGraph.Connected) (two : 1 < Nat.card ↥c.blocks) (B : ↥c.blocks) : (G.edgeCut {v : V | v ∈ ↑B}).Nonempty

In a connected multigraph, some edge leaves each block, unless there is only one.

def Cslib.Circuits.Frontier.Multigraph.Compression.external {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) : Set E

The external edges: those between distinct blocks.

theorem Cslib.Circuits.Frontier.Multigraph.Compression.compl_external {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) : c.externalᶜ = {e : E | ∃ B ∈ c.blocks, G.src e ∈ B ∧ G.tgt e ∈ B}

The edges outside the external edges are those inside a block.

noncomputable def Cslib.Circuits.Frontier.Multigraph.Compression.quotient {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) : Multigraph ↥c.blocks ↑c.external

The quotient of a compression: the multigraph whose vertices are the blocks and whose edges are the external edges, each joining the blocks of its endpoints.

@[simp]

theorem Cslib.Circuits.Frontier.Multigraph.Compression.quotient_src {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) (e : ↑c.external) : c.quotient.src e = c.blockOf (G.src ↑e)

@[simp]

theorem Cslib.Circuits.Frontier.Multigraph.Compression.quotient_tgt {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) (e : ↑c.external) : c.quotient.tgt e = c.blockOf (G.tgt ↑e)

theorem Cslib.Circuits.Frontier.Multigraph.Compression.quotient_loopless {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) : c.quotient.Loopless

theorem Cslib.Circuits.Frontier.Multigraph.Compression.edgeCut_preimage {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) (T : Set ↥c.blocks) : G.edgeCut (c.blockOf ⁻¹' T) = Subtype.val '' c.quotient.edgeCut T

The cut of a union of whole blocks consists of the edges of the cut of the quotient.

theorem Cslib.Circuits.Frontier.Multigraph.Compression.ncard_edgeCut_preimage {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) (T : Set ↥c.blocks) : (G.edgeCut (c.blockOf ⁻¹' T)).ncard = (c.quotient.edgeCut T).ncard

Cuts of unions of whole blocks are cuts of the quotient.

theorem Cslib.Circuits.Frontier.Multigraph.Compression.ncard_incidenceSet_quotient {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) (B : ↥c.blocks) : (c.quotient.incidenceSet B).ncard = (G.edgeCut {v : V | v ∈ ↑B}).ncard

The edges at a block of the quotient are the edges leaving the block.

theorem Cslib.Circuits.Frontier.Multigraph.Compression.quotient_maxDegreeLE {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) [Finite E] : c.quotient.MaxDegreeLE d

theorem Cslib.Circuits.Frontier.Multigraph.Compression.sum_ncard_edgeCut {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) [Finite E] : ∑ B : ↥c.blocks, (G.edgeCut {v : V | v ∈ ↑B}).ncard = 2 * Nat.card ↑c.external

The cuts of the blocks count every external edge twice.

theorem Cslib.Circuits.Frontier.Multigraph.Compression.card_add_card_external_le {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) [Finite E] : Nat.card V + Nat.card ↑c.external ≤ Nat.card ↥c.blocks + Nat.card E

The quotient is no more cyclic than the multigraph: |V| - |B| ≤ |E| - |E_B|, where B is the set of blocks and E_B the set of external edges.

Expansion

theorem Cslib.Circuits.Frontier.Multigraph.Compression.exists_width_le {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) [Finite V] [Finite E] (σ : Layout ↥c.blocks) : ∃ (π : Layout V), G.width π ≤ c.quotient.width σ + d * Nat.log 2 (Nat.card V)

Expansion. Lay out the vertices block by block, ordering the blocks by a layout σ of the quotient and each block by its list. Each frontier consists of whole blocks, which are cut by a frontier of σ, and a proper prefix of one more block. So the width exceeds that of σ by at most d log₂ |V|.