Documentation

CslibFrontier.Computability.Complexity.Problems.Partition

Partition #

Partition is the set of lists of natural numbers, possibly with repetitions, that split into two sub-multisets with equal sums [Kar72]. Numbers are encoded in binary (encNat).

Appending the two numbers a.sum + 1 and 2 * t + 1 to the numbers a reduces SubsetSum to Partition: together these two exceed half of the new total, so they lie on opposite sides of any partition, and the side holding a.sum + 1 holds numbers of a summing to exactly t. Neither number needs subtraction, so the reduction is defined for every target, including targets larger than a.sum.

Main definitions #

Main results #

References #

source
def Cslib.Complexity.Partition :
Set (List ℕ)

The lists of natural numbers that split into two sub-multisets with equal sums [Kar72].

Instances For
    source
    theorem Cslib.Complexity.mem_Partition_iff {l : List ℕ} :
    l ∈ Partition ↔ ∃ s ≤ ↑l, 2 * s.sum = l.sum

    A partition is a sub-multiset holding half of the total sum.

    source
    theorem Cslib.Complexity.mem_Partition_iff_sublist {l : List ℕ} :
    l ∈ Partition ↔ ∃ (s : List ℕ), s.Sublist l ∧ 2 * s.sum = l.sum

    A partition is a subsequence holding half of the total sum.

    source
    def Cslib.Complexity.Partition.verifier :
    List ℕ × List Bool → Bool

    The verifier for Partition, a mask verifier (Cslib.Complexity.maskVerifier): the numbers selected by the certificate mask hold half of the total sum.

    Instances For
      source
      theorem Cslib.Complexity.Partition.isVerifier :
      IsVerifier (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) Polynomial.X verifier Partition

      Partition.verifier verifies Partition with certificates as long as the encoded list.

      source
      theorem Cslib.Complexity.Partition.computableInPolyTime_verifier :
      Turing.MultiTapeTM.ComputableInPolyTime verifier (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

      The Partition verifier is polynomial-time.

      source
      theorem Cslib.Complexity.Partition.mem_NP :
      Partition ∈ NP (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

      Partition belongs to NP.

      source
      def Cslib.Complexity.SubsetSum.toPartition (x : SubsetSumInstance) :
      List ℕ

      The reduction from SubsetSum to Partition: append a.sum + 1 and 2 * t + 1.

      Instances For
        source
        theorem Cslib.Complexity.SubsetSum.toPartition_mem_iff (x : SubsetSumInstance) :
        toPartition x ∈ Partition ↔ x ∈ SubsetSum

        Correctness of the reduction to Partition.

        source
        theorem Cslib.Complexity.SubsetSum.computableInPolyTime_toPartition :
        Turing.MultiTapeTM.ComputableInPolyTime toPartition encSubsetSum (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

        The reduction to Partition is polynomial-time.

        source
        theorem Cslib.Complexity.polyTimeReducible_SubsetSum_Partition :
        PolyTimeReducible encSubsetSum (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) SubsetSum Partition

        SubsetSum reduces to Partition in polynomial time.

        source
        theorem Cslib.Complexity.Partition_npHard :
        NPHard (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) Partition

        Partition is NP-hard.

        source
        theorem Cslib.Complexity.Partition_npComplete :
        NPComplete (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) Partition

        Partition is NP-complete, with the numbers in binary [Kar72].