Biclique edge cover

AbbreviationBiclique edge cover instances#✓fully proved

An instance of BICLIQUE EDGE COVER is a tuple \((L, R, E, K)\) of natural numbers \(L\), \(R\) and \(K\) and a finite list \(E\) of pairs of natural numbers. Here \(L\) counts the left vertices, \(R\) counts the right vertices, each pair \((a, b)\) in \(E\) is an edge from left vertex \(a\) to right vertex \(b\), and \(K\) is the bound on the number of bicliques.

abbrev BicliqueEdgeCoverInstance := ℕ × ℕ × List (ℕ × ℕ) × ℕ

Used by 3

Used byThe biclique edge cover decision problem · Feasible biclique edge cover instances · Well-formed biclique edge cover instances

DefinitionWell-formed biclique edge cover instances#✓fully proved

An instance \((L, R, E, K)\) of BICLIQUE EDGE COVER is well formed when the list \(E\) has no repeated entries and every pair \((a, b)\) in \(E\) satisfies \(a < L\) and \(b < R\).

def WellFormed (i : BicliqueEdgeCoverInstance) : Prop :=
  i.2.2.1.Nodup ∧ ∀ e ∈ i.2.2.1, e.1 < i.1 ∧ e.2 < i.2.1

Uses 1 · Used by 1

Statement usesBiclique edge cover instances

Used byThe biclique edge cover decision problem

DefinitionFeasible biclique edge cover instances#✓fully proved

An instance \((L, R, E, K)\) of BICLIQUE EDGE COVER is feasible when there is a list of at most \(K\) pairs \((A, B)\) of finite lists of natural numbers, with every element of \(A\) less than \(L\) and every element of \(B\) less than \(R\), such that for every pair \((u, v)\) in \(E\) some listed pair \((A, B)\) has \(u \in A\), \(v \in B\) and \((a, b)\) in \(E\) for all \(a \in A\) and \(b \in B\).

def BicliqueEdgeCoverFeasible
    (i : BicliqueEdgeCoverInstance) : Prop :=
  ∃ bicliques : List (List ℕ × List ℕ), bicliques.length ≤ i.2.2.2 ∧
    (∀ p ∈ bicliques, (∀ a ∈ p.1, a < i.1) ∧ ∀ b ∈ p.2, b < i.2.1) ∧
    ∀ e ∈ i.2.2.1, ∃ p ∈ bicliques, e.1 ∈ p.1 ∧ e.2 ∈ p.2 ∧
      ∀ a ∈ p.1, ∀ b ∈ p.2, (a, b) ∈ i.2.2.1

Uses 1 · Used by 1

Statement usesBiclique edge cover instances

Used byThe biclique edge cover decision problem

DefinitionThe biclique edge cover decision problem#✓fully proved

BICLIQUE EDGE COVER is the decision problem that accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding of biclique edge cover instances, to an instance that is well formed and feasible; it rejects every bitstring that fails to decode.

noncomputable def bicliqueEdgeCoverDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := BicliqueEdgeCoverInstance) x with
  | some i => decide (WellFormed i ∧ BicliqueEdgeCoverFeasible i)
  | none => false

Uses 12 · Used by 1

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Feasible biclique edge cover instances · Biclique edge cover instances · Well-formed biclique edge cover instances · Decision problems

Used byBICLIQUE EDGE COVER is NP-complete

TheoremBICLIQUE EDGE COVER is NP-complete#●ready to prove

The biclique edge cover decision problem belongs to NP, and every decision problem in NP has a polynomial-time many-one reduction to it.

public theorem_wanted bicliqueEdgeCover_npComplete :
    bicliqueEdgeCoverDec ∈ MetaMathlibExt.ComplexityTheory.NP ∧
      ∀ L : MetaMathlibExt.ComplexityTheory.DecisionProblem,
        L ∈ MetaMathlibExt.ComplexityTheory.NP →
          Cslib.CookLevin.PolyManyOneRed L bicliqueEdgeCoverDec

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), BICLIQUE COVER.

Uses 5

Statement usesPolynomial-time many-one reduction · The biclique edge cover decision problem · Complexity classes · Decision problems · The complexity class NP

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.