#ExactCover: counting exact covers

The counting version of DescriptiveComplexity.ExactCover: the number of subfamilies of a set system covering every ground element exactly once (DescriptiveComplexity.ExactCoverBy). A cover is a set of members of the family, so nothing has to be said about the other elements of the instance.

DescriptiveComplexity.SharpExactCover is in #P (DescriptiveComplexity.sharpExactCover_mem_sharpP); its parsimonious hardness is in DescriptiveComplexity.Problems.ExactCoverCounting.

def DescriptiveComplexity.familyGuessOf {A : Type} (G : A → Prop) : familyGuessBlock.Assignment A

Subfamilies, as assignments of the guess block with an empty binary relation.

Equations

• DescriptiveComplexity.familyGuessOf G DescriptiveComplexity.FamilyGuessBlockIx.guess = fun (w : Fin 1 → A) => G (w 0)
• DescriptiveComplexity.familyGuessOf G DescriptiveComplexity.FamilyGuessBlockIx.inj = fun (x : Fin 2 → A) => False

def DescriptiveComplexity.exactCoverEquiv (A : Type) [FirstOrder.Language.setSystem.Structure A] : { ρ : familyGuessBlock.Assignment A // A ⊨ sharpExactCoverKernel } ≃ { G : A → Prop // ExactCoverBy SSElem SSFam SSMem G }

The exact covers of a set system are the witnesses of the counting kernel, bijectively.

Equations

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

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

#ExactCover: the number of exact covers of a set system.

Equations

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

theorem DescriptiveComplexity.sharpExactCover_support_iff (A : Type) [FirstOrder.Language.setSystem.Structure A] [Finite A] : SharpExactCover.support.Holds A ↔ ExactCover.Holds A

The support of #ExactCover is Exact Cover. Registered in the Lax archive as Lax280166.ExactCoverComplete.sharpExactCover_support_iff.

theorem DescriptiveComplexity.sharpExactCover_mem_sharpP : SharpP.Mem SharpExactCover

#ExactCover is in #P.