Documentation

DescriptiveComplexity.OccurrenceSlack

Slack occurrences of a clause #

Semantic layer shared by the two gadgets that ask a digit block to split in half: Partition (DescriptiveComplexity.Problems.Partition.Hardness) and job sequencing (DescriptiveComplexity.Problems.JobSequencing.Hardness). Both give a clause of width w one item per occurrence plus one per slack occurrence (DescriptiveComplexity.SatOcc.Mid) – an occurrence that is neither the first nor the last one, of which there are w − 2. The block then totals w + (w − 2), an even number, and a balanced split takes between 1 and w − 1 true literals, which is exactly not-all-equal satisfaction.

Besides the predicate and its formula (DescriptiveComplexity.SatOcc.midF), this file holds the two cardinality facts both gadgets need: a clause with an occurrence has strictly fewer slack occurrences than occurrences (DescriptiveComplexity.SatOcc.card_midSet_lt), and one with at least two occurrences has exactly two fewer (DescriptiveComplexity.SatOcc.card_midSet_add_two) – its first and its last.

Slack occurrences #

source
def DescriptiveComplexity.SatOcc.Mid {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (c x : A) (s : Bool) :
Prop

A slack occurrence of a clause: an occurrence that is neither the first nor the last one. A clause of width w ≥ 1 has w − 2 of them (or none, if w = 1), which is exactly the slack a balanced split needs.

Equations
Instances For
    Dependency graph
    source
    theorem DescriptiveComplexity.SatOcc.Mid.occIn {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {c x : A} {s : Bool} (h : Mid c x s) :
    OccIn c x s
    Dependency graph
    source
    noncomputable def DescriptiveComplexity.SatOcc.midF {α : Type} (s : Bool) (c x : α) :
    satOrd.Formula α

    A slack occurrence of c, as a formula.

    Equations
    Instances For
      Dependency graph
      source
      @[simp]
      theorem DescriptiveComplexity.SatOcc.realize_midF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {α : Type} {v : α → A} {s : Bool} {c x : α} :
      (midF s c x).Realize v ↔ Mid (v c) (v x) s
      Dependency graph

      The occurrences of a clause, and its slack #

      source
      def DescriptiveComplexity.SatOcc.OccSet {A : Type} [FirstOrder.Language.sat.Structure A] (c : A) :
      Set (A × Bool)

      The occurrences of a clause, as a set of signed positions.

      Equations
      Instances For
        Dependency graph
        source
        def DescriptiveComplexity.SatOcc.MidSet {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (c : A) :
        Set (A × Bool)

        The slack occurrences of a clause.

        Equations
        Instances For
          Dependency graph
          source
          theorem DescriptiveComplexity.SatOcc.midSet_subset {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {c : A} :
          MidSet c ⊆ OccSet c
          Dependency graph
          source
          theorem DescriptiveComplexity.SatOcc.minOcc_unique {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {c x y : A} {s t : Bool} (h : MinOcc c x s) (h' : MinOcc c y t) :
          (x, s) = (y, t)

          The first occurrence of a clause is unique.

          Dependency graph
          source
          theorem DescriptiveComplexity.SatOcc.maxOcc_unique {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {c x y : A} {s t : Bool} (h : MaxOcc c x s) (h' : MaxOcc c y t) :
          (x, s) = (y, t)

          The last occurrence of a clause is unique.

          Dependency graph
          source
          theorem DescriptiveComplexity.SatOcc.card_midSet_lt {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {c : A} (hne : (OccSet c).Nonempty) :
          (MidSet c).ncard < (OccSet c).ncard

          A clause with an occurrence has strictly fewer slack occurrences than occurrences: its first one is not one of them.

          Dependency graph
          source
          theorem DescriptiveComplexity.SatOcc.card_midSet_add_two {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {c : A} (h2 : 2 ≤ (OccSet c).ncard) :
          (MidSet c).ncard + 2 = (OccSet c).ncard

          A clause with at least two occurrences has exactly two fewer slack occurrences: its first and its last one.

          Dependency graph