Documentation

DescriptiveComplexity.Problems.ExactCoverCounting

#ExactCover is parsimoniously #P-complete #

The reduction of 1-in-SAT to Exact Cover in DescriptiveComplexity.Problems.ExactCover is parsimonious as it stands: covering the element of a variable exactly once is choosing one of its two literals, so the exact covers of the literal set system are the exactly-one models of the formula, bijectively (DescriptiveComplexity.ExactCoverRed.modelEquiv). No order, no gadget, dimension 1.

The one thing counting asks of that reduction is that only the variables of the formula be ground elements: an element occurring in no clause would otherwise be covered by either of two singleton sets.

source
def DescriptiveComplexity.ExactCoverRed.modelEquiv (A : Type) [FirstOrder.Language.sat.Structure A] :
{ ν : A → Prop // OneInModel A ν } ≃ { G : ecInterp.Map A → Prop // ExactCoverBy SSElem SSFam SSMem G }

The exact covers of the literal set system are the exactly-one models of the formula, bijectively.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Dependency graph
    source
    theorem DescriptiveComplexity.ExactCoverRed.sharpExactCover_map (A : Type) [FirstOrder.Language.sat.Structure A] :
    SharpExactCover.Count (ecInterp.Map A) = SharpOneInSAT.Count A

    Correctness of the interpretation, for counting.

    Dependency graph
    source
    noncomputable def DescriptiveComplexity.sharpOneInSat_parsimonious_sharpExactCover :
    ParsimoniousReduction SharpOneInSAT SharpExactCover

    #1-in-SAT reduces parsimoniously to #ExactCover, without an order.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Dependency graph
      source
      theorem DescriptiveComplexity.sharpExactCover_sharpP_parsimoniousHard :
      SharpP.ParsimoniousHard SharpExactCover

      #ExactCover is parsimoniously #P-hard.

      Dependency graph
      source
      theorem DescriptiveComplexity.sharpExactCover_sharpP_parsimoniousComplete :
      SharpP.ParsimoniousComplete SharpExactCover

      #ExactCover is parsimoniously #P-complete. Registered in the Lax archive as Lax280166.ExactCoverComplete.sharpExactCover_sharpP_parsimoniousComplete.

      Dependency graph
      source
      theorem DescriptiveComplexity.sharpExactCover_sharpP_complete :
      SharpP.Complete SharpExactCover

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

      Dependency graph