#Set Packing

The counting version of DescriptiveComplexity.SetPacking: the number of pairwise disjoint subfamilies with exactly as many sets as the marked set (DescriptiveComplexity.PackingOfSize). It is parsimoniously #P-complete (DescriptiveComplexity.sharpSetPacking_sharpP_parsimoniousComplete).

Membership is the generic argument for a solution of the threshold size (DescriptiveComplexity.sharpPDefinable_of_sized_set), the order-free part being “the subfamily is a packing”. Hardness is the edge-incidence interpretation of DescriptiveComplexity.Problems.SetFamily.FromGraphs unchanged: the sets of the interpreted system are the vertices, one each, so its packings of a size are the independent sets of that size, bijectively (DescriptiveComplexity.packEquiv).

def DescriptiveComplexity.PackingOfSize (A : Type) [FirstOrder.Language.setSystem.Structure A] (G : A → Prop) : Prop

The subfamily G is a packing with exactly as many sets as the marked set, in a finite set system.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.PackingOfSize.map {A : Type} [FirstOrder.Language.setSystem.Structure A] {B : Type} [FirstOrder.Language.setSystem.Structure B] (e : FirstOrder.Language.setSystem.Equiv A B) {G : A → Prop} (h : PackingOfSize A G) : PackingOfSize B fun (b : B) => G (e.symm b)

Packings of the threshold size transport along an isomorphism.

noncomputable def DescriptiveComplexity.SharpSetPacking : CountingProblem FirstOrder.Language.setSystem

#Set Packing: the number of pairwise disjoint subfamilies with exactly as many sets as the marked set.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.sharpSetPacking_support_iff (A : Type) [FirstOrder.Language.setSystem.Structure A] [Finite A] : SharpSetPacking.support.Holds A ↔ SetPacking.Holds A

The support of #Set Packing is Set Packing: a packing at least as large as the marked set contains one of exactly that size. Registered in the Lax archive as Lax280166.SetPackingComplete.sharpSetPacking_support_iff.

Membership

@[reducible, inline]

abbrev DescriptiveComplexity.psSelSym : packSelLang.Relations 1

The sel symbol over the sum.

Equations

• DescriptiveComplexity.psSelSym = Sum.inr DescriptiveComplexity.psSelRel

@[reducible, inline]

abbrev DescriptiveComplexity.packSelLang : FirstOrder.Language

The vocabulary of the kernel: the instance expanded by the block.

Equations

• DescriptiveComplexity.packSelLang = FirstOrder.Language.setSystem.sum DescriptiveComplexity.packSelBlock.lang

def DescriptiveComplexity.packSelBlock : SOBlock

The block of the counting definition of Set Packing: the packing itself.

Equations

• One or more equations did not get rendered due to their size.

def DescriptiveComplexity.psSelRel : packSelBlock.lang.Relations 1

The sel relation variable.

Equations

• DescriptiveComplexity.psSelRel = ⟨DescriptiveComplexity.PackSelBlockIx.sel, DescriptiveComplexity.psSelRel._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.psMemSym : packSelLang.Relations 2

The mem symbol over the sum.

Equations

• DescriptiveComplexity.psMemSym = Sum.inl FirstOrder.Language.ssMem

@[reducible, inline]

abbrev DescriptiveComplexity.psMarkedSym : packSelLang.Relations 1

The marked symbol over the sum.

Equations

• DescriptiveComplexity.psMarkedSym = Sum.inl FirstOrder.Language.ssMarked

@[reducible, inline]

abbrev DescriptiveComplexity.psFamSym : packSelLang.Relations 1

The fam symbol over the sum.

Equations

• DescriptiveComplexity.psFamSym = Sum.inl FirstOrder.Language.ssFam

inductive DescriptiveComplexity.PackSelBlockIx : Type

The relation variables of the block.

• sel : PackSelBlockIx

  The packing.

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqPackSelBlockIx : DecidableEq PackSelBlockIx

Equations

• DescriptiveComplexity.instDecidableEqPackSelBlockIx x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[reducible, inline]

abbrev DescriptiveComplexity.psElemSym : packSelLang.Relations 1

The elem symbol over the sum.

Equations

• DescriptiveComplexity.psElemSym = Sum.inl FirstOrder.Language.ssElem

@[instance_reducible]

instance DescriptiveComplexity.instFintypePackSelBlockIx : Fintype PackSelBlockIx

Equations

• DescriptiveComplexity.instFintypePackSelBlockIx = { elems := [DescriptiveComplexity.PackSelBlockIx.sel].toFinset, complete := DescriptiveComplexity.instFintypePackSelBlockIx._proof_1 }

instance DescriptiveComplexity.instSubsingletonιPackSelBlock : Subsingleton packSelBlock.ι

Hardness

theorem DescriptiveComplexity.packingOfSize_vertexFamily {A : Type} [FirstOrder.Language.markedGraph.Structure A] {S : A → Prop} (h : IndepOfSize A S) : PackingOfSize (edgeIncidenceInterp.Map A) (vertexFamily S)

The vertex-sets of an independent set of the threshold size are a packing of the threshold size.

theorem DescriptiveComplexity.packing_diag {A : Type} [FirstOrder.Language.markedGraph.Structure A] {G : edgeIncidenceInterp.Map A → Prop} (h : PackingOfSize (edgeIncidenceInterp.Map A) G) (p : edgeIncidenceInterp.Map A) : G p → ∃ (v : A), p = diagPt v

A packing of the interpreted system consists of vertex-sets.

theorem DescriptiveComplexity.indepOfSize_of_packing {A : Type} [FirstOrder.Language.markedGraph.Structure A] {G : edgeIncidenceInterp.Map A → Prop} (h : PackingOfSize (edgeIncidenceInterp.Map A) G) : IndepOfSize A fun (v : A) => G (diagPt v)

The vertices of a packing of the threshold size are an independent set of the threshold size.

def DescriptiveComplexity.packEquiv (A : Type) [FirstOrder.Language.markedGraph.Structure A] : { S : A → Prop // IndepOfSize A S } ≃ { G : edgeIncidenceInterp.Map A → Prop // PackingOfSize (edgeIncidenceInterp.Map A) G }

The packings of the threshold size of the edge-incidence system are the independent sets of the threshold size, bijectively.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.sharpIndependentSet_parsimonious_sharpSetPacking : ParsimoniousReduction SharpIndependentSet SharpSetPacking

#Independent Set reduces parsimoniously to #Set Packing, by the edge-incidence interpretation.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.sharpSetPacking_sharpP_parsimoniousHard : SharpP.ParsimoniousHard SharpSetPacking

#Set Packing is parsimoniously #P-hard.

theorem DescriptiveComplexity.sharpSetPacking_sharpP_parsimoniousComplete : SharpP.ParsimoniousComplete SharpSetPacking

#Set Packing is parsimoniously #P-complete, counting the packings of exactly the threshold size. Registered in the Lax archive as Lax280166.SetPackingComplete.sharpSetPacking_sharpP_parsimoniousComplete.

theorem DescriptiveComplexity.sharpSetPacking_sharpP_complete : SharpP.Complete SharpSetPacking

SharpSetPacking is #P-complete: parsimoniously, hence under subtractive reductions.