Graph cover transference

Rows and columns are supplied sets for bipartite graphs. When vertices are bit strings, each literal is a union of rows or columns. Consequently every graph witness is a Boolean literal witness, and a Boolean pair cover is already a graph pair cover, with the same length.

We use a pair of length-n bit strings for the Boolean input of length 2n. This is just the usual two-block encoding; the graph and Boolean problems share their ambient type. The result holds for every admissibility predicate, including semi-ultrafilters, and for trivial graphs.

Main definitions

• Cslib.Circuits.Fusion.Graph.sources: all rows followed by all columns.
• Cslib.Circuits.Fusion.Graph.literals: positive and negative literals on two bit-string blocks.

Main results

• Cslib.Circuits.Fusion.Graph.pairCoverComplexity_le_literals: graph cover bounds transfer without loss to Boolean literal cover bounds.

References

• B. P. Cavalar and I. C. Oliveira, Boolean Circuit Complexity and Two-Dimensional Cover Problems, Lemmas 39 and 48.

def Cslib.Circuits.Fusion.Graph.sources {V : Type u_1} [Fintype V] : Fin (Fintype.card V + Fintype.card V) → Set (V × V)

All rows, then all columns, of the complete bipartite ambient space.

theorem Cslib.Circuits.Fusion.Graph.row_source {V : Type u_1} [Fintype V] (v : V) : sources (Fin.castAdd (Fintype.card V) ((Fintype.equivFin V) v)) = {x : V × V | x.1 = v}

Each row is a supplied graph source.

theorem Cslib.Circuits.Fusion.Graph.column_source {V : Type u_1} [Fintype V] (v : V) : sources (Fin.natAdd (Fintype.card V) ((Fintype.equivFin V) v)) = {x : V × V | x.2 = v}

Each column is a supplied graph source.

def Cslib.Circuits.Fusion.Graph.literals {n : ℕ} (x : (Fin n → Bool) × (Fin n → Bool)) : Fin (n + n + (n + n)) → Bool

The four literal blocks: positive left, positive right, negative left, negative right.

theorem Cslib.Circuits.Fusion.Graph.literals_sourceRefinement {n : ℕ} (x : (Fin n → Bool) × (Fin n → Bool)) (i : Fin (n + n + (n + n))) (hi : literals x i = true) : ∃ (j : Fin (Fintype.card (Fin n → Bool) + Fintype.card (Fin n → Bool))), x ∈ sources j ∧ sources j ⊆ {y : (Fin n → Bool) × (Fin n → Bool) | literals y i = true}

Every literal containing a pair contains its row or its column.

theorem Cslib.Circuits.Fusion.Graph.pairCoverComplexity_le_literals {n : ℕ} (graph : Set ((Fin n → Bool) × (Fin n → Bool))) (admissible : Semifilter ↑graphᶜ → Prop := fun (x : Semifilter ↑graphᶜ) => True) : pairCoverComplexity graph sources admissible ≤ pairCoverComplexity graph (fun (i : Fin (n + n + (n + n))) => {x : (Fin n → Bool) × (Fin n → Bool) | literals x i = true}) admissible

Cavalar–Oliveira's graph-to-Boolean cover transfer (Lemmas 39 and 48). The arbitrary admissibility predicate includes both unrestricted semifilters and semi-ultrafilters.