Documentation

DescriptiveComplexity.Problems.ThreeColorability.SatGadget

The 3-coloring gadget graph of a CNF structure #

Combinatorial core of the reduction from SAT to 3-colorability: the classical gadget graph associated to a CNF, and the proof that it is 3-colorable iff the CNF is satisfiable. The first-order definition of this graph (as a tagged 2-dimensional interpretation) is in DescriptiveComplexity.Problems.ThreeColorability.FromSat; here everything is purely semantic.

Vertices are tagged pairs (t, a, b) with t : SatTag and a b elements of the CNF structure:

Junk vertices (tuples not matching the shapes above) have no incident edges.

The main result is DescriptiveComplexity.SatToCol.satisfiable_iff_gadColoring.

source
inductive DescriptiveComplexity.SatToCol.SatTag :
Type

Tags of the gadget graph.

  • palT : SatTag

    Palette “true”.

  • palF : SatTag

    Palette “false”.

  • palB : SatTag

    Palette “base”.

  • lit (s : Bool) : SatTag

    Literal vertex, at diagonal pairs (x, x).

  • gu (s : Bool) : SatTag

    OR-gate input from the previous prefix node, at pairs (c, x).

  • gv (s : Bool) : SatTag

    OR-gate input from the literal vertex, at pairs (c, x).

  • go (s : Bool) : SatTag

    OR-gate output, at pairs (c, x).

  • spoil : SatTag

    Spoiler for empty clauses, at diagonal pairs (c, c).

Instances For
    Dependency graph
    source
    @[instance_reducible]
    instance DescriptiveComplexity.SatToCol.instDecidableEqSatTag :
    DecidableEq SatTag
    Equations
    Dependency graph
    source
    def DescriptiveComplexity.SatToCol.instDecidableEqSatTag.decEq (x✝ x✝¹ : SatTag) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      Dependency graph
      source
      @[instance_reducible]
      instance DescriptiveComplexity.SatToCol.instFintypeSatTag :
      Fintype SatTag
      Equations
      Dependency graph
      source
      instance DescriptiveComplexity.SatToCol.instNonemptySatTag :
      Nonempty SatTag
      Dependency graph
      source
      def DescriptiveComplexity.SatToCol.Core {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] :
      SatTag → A → A → SatTag → A → A → Prop

      One direction of the edge relation of the gadget graph, in component form: Core t₁ a₁ b₁ t₂ a₂ b₂ relates the vertex (t₁, (a₁, b₁)) to (t₂, (a₂, b₂)). The edge relation of the graph is its symmetrization.

      Equations
      Instances For
        Dependency graph

        From a satisfying assignment to a proper coloring #

        source
        noncomputable def DescriptiveComplexity.SatToCol.gadCol {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (ν : A → Prop) :
        SatTag → A → A → Fin 3

        The coloring of the gadget graph induced by an assignment ν: 0 is “true”, 1 is “false”, 2 is “base”.

        Equations
        Instances For
          Dependency graph
          source
          theorem DescriptiveComplexity.SatToCol.gadCol_proper {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {ν : A → Prop} (hν : ∀ (c : A), SatOcc.IsCl c → ∃ (x : A) (s : Bool), SatOcc.OccIn c x s ∧ SatOcc.LitTrue ν x s) {t₁ t₂ : SatTag} {a₁ b₁ a₂ b₂ : A} (h : Core t₁ a₁ b₁ t₂ a₂ b₂) :
          gadCol ν t₁ a₁ b₁ ≠ gadCol ν t₂ a₂ b₂

          The coloring induced by a satisfying assignment is proper.

          Dependency graph

          Main combinatorial equivalence #

          source
          theorem DescriptiveComplexity.SatToCol.satisfiable_iff_gadColoring (A : Type) [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] :
          Satisfiable A ↔ ∃ (col : SatTag → A → A → Fin 3), ∀ (t₁ : SatTag) (a₁ b₁ : A) (t₂ : SatTag) (a₂ b₂ : A), Core t₁ a₁ b₁ t₂ a₂ b₂ → col t₁ a₁ b₁ ≠ col t₂ a₂ b₂

          Combinatorial correctness of the SAT → 3COL gadget: a CNF structure is satisfiable iff its gadget graph admits a proper 3-coloring.

          Dependency graph