Documentation

DescriptiveComplexity.Problems.SetSplitting

Set Splitting is NP-complete #

SET SPLITTING, also known as hypergraph 2-colorability: can the ground elements of a set system be colored with two colors so that no set of the family is monochromatic? Like Exact Cover it lives on FirstOrder.Language.setSystem unchanged (DescriptiveComplexity.SetSplitting, DescriptiveComplexity.Problems.SetFamily.Defs) and carries no threshold – the coloring, not a cardinality, is the whole question.

Hardness comes from NAE-SAT (DescriptiveComplexity.Problems.NaeSat) by a reduction with no gadget and no counting, order-free and of dimension 1:

A two-coloring splits the pair {x, ¬x} exactly when it gives the two literals of x opposite colors – that is a truth assignment – and it splits a clause set exactly when the clause has both a true and a false literal, which is not-all-equal satisfaction. The correspondence is so direct that the reduction is essentially the identity on clauses; only the pair sets are new, and they are what turns an arbitrary coloring into an assignment.

source
inductive DescriptiveComplexity.SetSplitRed.SplTag :
Type

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

  • lit (s : Bool) : SplTag

    The ground element of the literal (x, s).

  • pairSet : SplTag

    The set {x, ¬x} of the variable x.

  • clSet : SplTag

    The set of the literals of a clause.

Instances For
    Dependency graph
    source
    @[instance_reducible]
    instance DescriptiveComplexity.SetSplitRed.instDecidableEqSplTag :
    DecidableEq SplTag
    Equations
    Dependency graph
    source
    def DescriptiveComplexity.SetSplitRed.instDecidableEqSplTag.decEq (x✝ x✝¹ : SplTag) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      Dependency graph
      source
      @[instance_reducible]
      instance DescriptiveComplexity.SetSplitRed.instFintypeSplTag :
      Fintype SplTag
      Equations
      • One or more equations did not get rendered due to their size.
      Dependency graph
      source
      instance DescriptiveComplexity.SetSplitRed.instNonemptySplTag :
      Nonempty SplTag
      Dependency graph

      The interpretation #

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

      Defining formula for the ground elements: the literals.

      Equations
      Instances For
        Dependency graph
        source
        noncomputable def DescriptiveComplexity.SetSplitRed.famF :
        SplTag → FirstOrder.Language.sat.Formula (Fin 1 × Fin 1)

        Defining formula for the family: one set per variable and one per clause.

        Equations
        Instances For
          Dependency graph
          source
          noncomputable def DescriptiveComplexity.SetSplitRed.memF :
          SplTag → SplTag → FirstOrder.Language.sat.Formula (Fin 2 × Fin 1)

          Defining formula for incidence: the pair set of x holds both literals of x, and the set of a clause holds the literals occurring in it.

          Equations
          Instances For
            Dependency graph
            source
            noncomputable def DescriptiveComplexity.SetSplitRed.splInterp :
            FOInterpretation FirstOrder.Language.sat FirstOrder.Language.setSystem SplTag 1

            The interpretation of Set Splitting instances in CNF instances.

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

              The points #

              source
              def DescriptiveComplexity.SetSplitRed.splPt {A : Type} (t : SplTag) (x : A) :
              splInterp.Map A

              The point of tag t over the element x.

              Equations
              Instances For
                Dependency graph

                Characterization of the four relations #

                source
                @[simp]
                theorem DescriptiveComplexity.SetSplitRed.ssElem_lit {A : Type} [FirstOrder.Language.sat.Structure A] (s : Bool) (x : A) :
                SSElem (splPt (SplTag.lit s) x)
                Dependency graph
                source
                @[simp]
                theorem DescriptiveComplexity.SetSplitRed.ssElem_pairSet {A : Type} [FirstOrder.Language.sat.Structure A] (x : A) :
                ¬SSElem (splPt SplTag.pairSet x)
                Dependency graph
                source
                @[simp]
                theorem DescriptiveComplexity.SetSplitRed.ssElem_clSet {A : Type} [FirstOrder.Language.sat.Structure A] (x : A) :
                ¬SSElem (splPt SplTag.clSet x)
                Dependency graph
                source
                @[simp]
                theorem DescriptiveComplexity.SetSplitRed.ssFam_pairSet {A : Type} [FirstOrder.Language.sat.Structure A] (x : A) :
                SSFam (splPt SplTag.pairSet x)
                Dependency graph
                source
                @[simp]
                theorem DescriptiveComplexity.SetSplitRed.ssFam_clSet {A : Type} [FirstOrder.Language.sat.Structure A] (c : A) :
                SSFam (splPt SplTag.clSet c) ↔ SatOcc.IsCl c
                Dependency graph
                source
                @[simp]
                theorem DescriptiveComplexity.SetSplitRed.ssFam_lit {A : Type} [FirstOrder.Language.sat.Structure A] (s : Bool) (x : A) :
                ¬SSFam (splPt (SplTag.lit s) x)
                Dependency graph
                source
                @[simp]
                theorem DescriptiveComplexity.SetSplitRed.ssMem_lit_pairSet {A : Type} [FirstOrder.Language.sat.Structure A] (s : Bool) (x y : A) :
                SSMem (splPt (SplTag.lit s) x) (splPt SplTag.pairSet y) ↔ x = y
                Dependency graph
                source
                @[simp]
                theorem DescriptiveComplexity.SetSplitRed.ssMem_lit_clSet {A : Type} [FirstOrder.Language.sat.Structure A] (s : Bool) (x c : A) :
                SSMem (splPt (SplTag.lit s) x) (splPt SplTag.clSet c) ↔ SatOcc.OccIn c x s
                Dependency graph

                Correctness #

                source
                theorem DescriptiveComplexity.SetSplitRed.naeSatisfiable_iff_hasSetSplitting (A : Type) [FirstOrder.Language.sat.Structure A] :
                NAESatisfiable A ↔ HasSetSplitting (splInterp.Map A)

                Correctness of the reduction: a CNF structure is not-all-equal satisfiable iff its literal set system can be split.

                Dependency graph
                source
                noncomputable def DescriptiveComplexity.naeSat_fo_reduction_setSplitting :
                FOReduction NAESAT SetSplitting

                NAE-SAT FO-reduces to Set Splitting: the ground elements are the literals, the family holds one pair set per variable and one set per clause. No order, no gadget and no counting.

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

                  NP-completeness #

                  source
                  theorem DescriptiveComplexity.setSplitting_mem_NP :
                  NP.Mem SetSplitting

                  Set Splitting is in NP: it is Σ₁-definable.

                  Dependency graph
                  source
                  theorem DescriptiveComplexity.setSplitting_NP_hard :
                  NP.Hard SetSplitting

                  Set Splitting is NP-hard: NAE-SAT, which is NP-hard, FO-reduces to it.

                  Dependency graph
                  source
                  theorem DescriptiveComplexity.setSplitting_NP_complete :
                  NP.Complete SetSplitting

                  Set Splitting is NP-complete, derived from the first-order reductions of this library and the Cook–Levin theorem. Registered in the Lax archive as Lax799700.SetFamily.setSplitting_NP_complete.

                  Dependency graph