Balanced biclique

AbbreviationBalanced biclique instances#✓fully proved

An instance of BALANCED BICLIQUE is a triple \((n, es, K)\) consisting of a natural number \(n\) (the number of vertices), a list \(es\) of pairs of natural numbers (the edges) and a natural number \(K\) (the bound).

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

Used by 4

Used byThe decision problem BALANCED BICLIQUE · Feasible balanced biclique instances · Graph of a balanced biclique instance · Well-formed balanced biclique instances

DefinitionGraph of a balanced biclique instance#✓fully proved

The graph of a balanced biclique instance \((n, es, K)\) is the simple graph on \(\{0, \dots, n-1\}\) in which distinct vertices \(u\) and \(v\) are adjacent when \((u, v)\) or \((v, u)\) belongs to \(es\).

def Graph (i : BalancedBicliqueInstance) : SimpleGraph (Fin i.1) :=
  Cslib.Complexity.Karp.edgeGraph i.1 i.2.1

Uses 2 · Used by 1

Statement usesGraph of an edge list · Balanced biclique instances

Used byFeasible balanced biclique instances

DefinitionWell-formed balanced biclique instances#✓fully proved

A balanced biclique instance \((n, es, K)\) is well formed when the entries of the list \(es\) are distinct and every pair \((u, v)\) in \(es\) satisfies \(u < n\), \(v < n\), \(u \neq v\) and \((v, u) \notin es\).

def WellFormed (i : BalancedBicliqueInstance) : Prop :=
  i.2.1.Nodup ∧ ∀ e ∈ i.2.1, e.1 < i.1 ∧ e.2 < i.1 ∧ e.1 ≠ e.2 ∧ (e.2, e.1) ∉ i.2.1

Uses 1 · Used by 1

Statement usesBalanced biclique instances

Used byThe decision problem BALANCED BICLIQUE

DefinitionFeasible balanced biclique instances#✓fully proved

A balanced biclique instance \((n, es, K)\) is feasible when there are disjoint sets \(A\) and \(B\) of exactly \(K\) vertices each in \(\{0, \dots, n-1\}\) such that every vertex of \(A\) is adjacent to every vertex of \(B\), where distinct vertices \(u\) and \(v\) are adjacent when \((u, v)\) or \((v, u)\) belongs to \(es\). In other words, the graph contains a complete bipartite subgraph \(K_{K,K}\), not necessarily induced.

def BalancedBicliqueFeasible
    (i : BalancedBicliqueInstance) : Prop :=
  ∃ A B : Finset (Fin i.1), A.card = i.2.2 ∧ B.card = i.2.2 ∧ Disjoint A B ∧
    ∀ a ∈ A, ∀ b ∈ B, (Graph i).Adj a b

Uses 2 · Used by 1

Statement usesBalanced biclique instances · Graph of a balanced biclique instance

Used byThe decision problem BALANCED BICLIQUE

DefinitionThe decision problem BALANCED BICLIQUE#✓fully proved

BALANCED BICLIQUE is the decision problem that accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to a balanced biclique instance \((n, es, K)\) that is well formed (the entries of \(es\) are distinct, and every pair \((u, v)\) in \(es\) has \(u < n\), \(v < n\), \(u \neq v\) and \((v, u) \notin es\)) and for which there are disjoint sets \(A\) and \(B\) of exactly \(K\) vertices each in \(\{0, \dots, n-1\}\) such that every vertex of \(A\) is adjacent to every vertex of \(B\), where distinct vertices \(u\) and \(v\) are adjacent when \((u, v)\) or \((v, u)\) belongs to \(es\). Bitstrings that do not decode are rejected.

noncomputable def balancedBicliqueDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := BalancedBicliqueInstance) x with
  | some i => decide (WellFormed i ∧ BalancedBicliqueFeasible 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 balanced biclique instances · Balanced biclique instances · Well-formed balanced biclique instances · Decision problems

Used byBALANCED BICLIQUE is NP-complete

TheoremBALANCED BICLIQUE is NP-complete#●ready to prove

The decision problem BALANCED BICLIQUE belongs to NP, and every decision problem in NP reduces to it by a polynomial-time many-one reduction.

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), BALANCED COMPLETE BIPARTITE SUBGRAPH; D. S. Johnson, "The NP- completeness column" (1987).

Uses 5

Statement usesPolynomial-time many-one reduction · The decision problem BALANCED BICLIQUE · Complexity classes · Decision problems · The complexity class NP

5 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.