Documentation

DescriptiveComplexity.Problems.ExactCover

Exact Cover is NP-complete #

EXACT COVER ([Karp 1972][karp1972reducibility]): is there a subfamily covering every ground element exactly once? The problem lives on FirstOrder.Language.setSystem unchanged (DescriptiveComplexity.ExactCover, DescriptiveComplexity.Problems.SetFamily.Defs) – exactness is a property of the subfamily, not a new vocabulary, and it replaces the threshold, so the marked set plays no role at all.

Hardness comes from exactly-one satisfiability (DescriptiveComplexity.Problems.OneInSat) by a reduction with no gadget and no counting, order-free and of dimension 1:

Covering the element x exactly once picks exactly one of the two literals of x – that is a truth assignment – and covering a clause exactly once is exactly what exactly-one satisfaction asks. Nothing here depends on the width of the clauses, which is why the source is unrestricted 1-in-SAT rather than its width-three restriction.

source
inductive DescriptiveComplexity.ExactCoverRed.ECTag :
Type

Tags of the reduction: the ground element of a variable, the ground element of a clause, and the set of a literal.

  • velt : ECTag

    The ground element of a variable.

  • celt : ECTag

    The ground element of a clause.

  • lset (s : Bool) : ECTag

    The set of the literal (x, s).

Instances For
    source
    @[instance_reducible]
    instance DescriptiveComplexity.ExactCoverRed.instDecidableEqECTag :
    DecidableEq ECTag
    Equations
    source
    def DescriptiveComplexity.ExactCoverRed.instDecidableEqECTag.decEq (x✝ x✝¹ : ECTag) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      @[instance_reducible]
      instance DescriptiveComplexity.ExactCoverRed.instFintypeECTag :
      Fintype ECTag
      Equations
      • One or more equations did not get rendered due to their size.
      source
      instance DescriptiveComplexity.ExactCoverRed.instNonemptyECTag :
      Nonempty ECTag

      The interpretation #

      source
      noncomputable def DescriptiveComplexity.ExactCoverRed.elemF :
      ECTag → FirstOrder.Language.sat.Formula (Fin 1 × Fin 1)

      Defining formula for the ground elements: the variables and the clauses.

      Equations
      Instances For
        source
        noncomputable def DescriptiveComplexity.ExactCoverRed.famF :
        ECTag → FirstOrder.Language.sat.Formula (Fin 1 × Fin 1)

        Defining formula for the family: one set per literal.

        Equations
        Instances For
          source
          noncomputable def DescriptiveComplexity.ExactCoverRed.memF :
          ECTag → ECTag → FirstOrder.Language.sat.Formula (Fin 2 × Fin 1)

          Defining formula for incidence: the set of (x, s) contains the element of x and the elements of the clauses where (x, s) occurs.

          Equations
          Instances For
            source
            noncomputable def DescriptiveComplexity.ExactCoverRed.ecInterp :
            FOInterpretation FirstOrder.Language.sat FirstOrder.Language.setSystem ECTag 1

            The interpretation of Exact Cover instances in CNF instances.

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

              The points #

              source
              def DescriptiveComplexity.ExactCoverRed.ecPt {A : Type} (t : ECTag) (x : A) :
              ecInterp.Map A

              The point of tag t over the element x.

              Equations
              Instances For
                source
                theorem DescriptiveComplexity.ExactCoverRed.ecPt_eq_iff {A : Type} {t t' : ECTag} {x x' : A} :
                ecPt t x = ecPt t' x' ↔ t = t' ∧ x = x'
                source
                theorem DescriptiveComplexity.ExactCoverRed.ecPt_surj {A : Type} (q : ecInterp.Map A) :
                ∃ (t : ECTag) (x : A), q = ecPt t x

                Characterization of the four relations #

                source
                @[simp]
                theorem DescriptiveComplexity.ExactCoverRed.ssElem_velt {A : Type} [FirstOrder.Language.sat.Structure A] (x : A) :
                SSElem (ecPt ECTag.velt x)
                source
                @[simp]
                theorem DescriptiveComplexity.ExactCoverRed.ssElem_celt {A : Type} [FirstOrder.Language.sat.Structure A] (c : A) :
                SSElem (ecPt ECTag.celt c) ↔ SatOcc.IsCl c
                source
                @[simp]
                theorem DescriptiveComplexity.ExactCoverRed.ssElem_lset {A : Type} [FirstOrder.Language.sat.Structure A] (s : Bool) (x : A) :
                ¬SSElem (ecPt (ECTag.lset s) x)
                source
                @[simp]
                theorem DescriptiveComplexity.ExactCoverRed.ssFam_lset {A : Type} [FirstOrder.Language.sat.Structure A] (s : Bool) (x : A) :
                SSFam (ecPt (ECTag.lset s) x)
                source
                @[simp]
                theorem DescriptiveComplexity.ExactCoverRed.ssFam_velt {A : Type} [FirstOrder.Language.sat.Structure A] (x : A) :
                ¬SSFam (ecPt ECTag.velt x)
                source
                @[simp]
                theorem DescriptiveComplexity.ExactCoverRed.ssFam_celt {A : Type} [FirstOrder.Language.sat.Structure A] (x : A) :
                ¬SSFam (ecPt ECTag.celt x)
                source
                @[simp]
                theorem DescriptiveComplexity.ExactCoverRed.ssMem_velt_lset {A : Type} [FirstOrder.Language.sat.Structure A] (x : A) (s : Bool) (y : A) :
                SSMem (ecPt ECTag.velt x) (ecPt (ECTag.lset s) y) ↔ x = y
                source
                @[simp]
                theorem DescriptiveComplexity.ExactCoverRed.ssMem_celt_lset {A : Type} [FirstOrder.Language.sat.Structure A] (c : A) (s : Bool) (x : A) :
                SSMem (ecPt ECTag.celt c) (ecPt (ECTag.lset s) x) ↔ SatOcc.OccIn c x s
                source
                theorem DescriptiveComplexity.ExactCoverRed.ssFam_cases {A : Type} [FirstOrder.Language.sat.Structure A] {q : ecInterp.Map A} (h : SSFam q) :
                ∃ (s : Bool) (x : A), q = ecPt (ECTag.lset s) x

                The sets of the family are exactly the literal sets.

                source
                theorem DescriptiveComplexity.ExactCoverRed.ssElem_cases {A : Type} [FirstOrder.Language.sat.Structure A] {q : ecInterp.Map A} (h : SSElem q) :
                (∃ (x : A), q = ecPt ECTag.velt x) ∨ ∃ (c : A), SatOcc.IsCl c ∧ q = ecPt ECTag.celt c

                The ground elements are exactly the variables and the clauses.

                Correctness #

                source
                theorem DescriptiveComplexity.ExactCoverRed.oneInSatisfiable_iff_hasExactCover (A : Type) [FirstOrder.Language.sat.Structure A] :
                OneInSatisfiable A ↔ HasExactCover (ecInterp.Map A)

                Correctness of the reduction: a CNF structure is exactly-one satisfiable iff its literal set system has an exact cover.

                source
                noncomputable def DescriptiveComplexity.oneInSat_fo_reduction_exactCover :
                FOReduction OneInSAT ExactCover

                1-in-SAT FO-reduces to Exact Cover: the ground elements are the variables and the clauses, and the family has one set per literal. No order, no gadget and no counting.

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

                  NP-completeness #

                  source
                  theorem DescriptiveComplexity.exactCover_NP_hard :
                  NP.Hard ExactCover

                  Exact Cover is NP-hard: 1-in-SAT, which is NP-hard, FO-reduces to it.

                  source
                  theorem DescriptiveComplexity.exactCover_NP_complete :
                  NP.Complete ExactCover

                  Exact Cover is NP-complete, derived from the first-order reductions of this library and the Cook–Levin theorem.