Set splitting

AbbreviationSet-splitting instances#✓fully proved

A set-splitting instance is a pair \((n, C)\) of a natural number \(n\), the size of the universe, and a list \(C\) of lists of natural numbers, the subsets to be split.

abbrev SetSplittingInstance := ℕ × List (List ℕ)

Used by 3

Used byThe SET SPLITTING decision problem · Feasible set-splitting instances · Well-formed set-splitting instances

DefinitionWell-formed set-splitting instances#✓fully proved

A set-splitting instance \((n, C)\), a natural number \(n\) together with a list \(C\) of lists of natural numbers, is well formed when every list in \(C\) has no repeated entries and all its entries are less than \(n\).

def WellFormed (i : SetSplittingInstance) : Prop :=
  ∀ s ∈ i.2, s.Nodup ∧ ∀ x ∈ s, x < i.1

Uses 1 · Used by 1

Statement usesSet-splitting instances

Used byThe SET SPLITTING decision problem

DefinitionFeasible set-splitting instances#✓fully proved

A set-splitting instance \((n, C)\), a natural number \(n\) together with a list \(C\) of lists of natural numbers, is feasible when there is a finite set \(S\) of natural numbers, all less than \(n\), such that every list in \(C\) has an entry in \(S\) and an entry not in \(S\).

def SetSplittingFeasible
    (i : SetSplittingInstance) : Prop :=
  ∃ S : Finset ℕ, (∀ v ∈ S, v < i.1) ∧
    ∀ s ∈ i.2, (∃ x ∈ s, x ∈ S) ∧ ∃ y ∈ s, y ∉ S

Uses 1 · Used by 1

Statement usesSet-splitting instances

Used byThe SET SPLITTING decision problem

DefinitionThe SET SPLITTING decision problem#✓fully proved

SET SPLITTING is the decision problem that accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to a pair \((n, C)\) of a natural number \(n\) and a list \(C\) of lists of natural numbers such that every list in \(C\) has no repeated entries and only entries less than \(n\), and some finite set \(S\) of natural numbers less than \(n\) contains an entry of every list in \(C\) and misses an entry of every list in \(C\). Bitstrings that do not decode to such a pair are rejected.

noncomputable def setSplittingDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := SetSplittingInstance) x with
  | some i => decide (WellFormed i ∧ SetSplittingFeasible 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 set-splitting instances · Set-splitting instances · Well-formed set-splitting instances · Decision problems

Used bySET SPLITTING is NP-complete

TheoremSET SPLITTING is NP-complete#●ready to prove

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

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability (1979), SET SPLITTING (hypergraph 2-coloring); S. Lovasz, "Coverings and colorings of hypergraphs" (1973).

Uses 5

Statement usesPolynomial-time many-one reduction · The SET SPLITTING 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.