Documentation

DescriptiveComplexity.Problems.ThreeColorability.FromSat

SAT reduces to 3-colorability by an ordered FO reduction #

The reverse direction of DescriptiveComplexity.Problems.ThreeColorability.ToSat: the gadget graph of DescriptiveComplexity.Problems.ThreeColorability.SatGadget is first-order definable over the ordered expansion Language.sat.sum Language.order of the language of CNF instances, giving an ordered first-order reduction from SAT to 3-colorability – DescriptiveComplexity.sat_ordered_fo_reduction_threeCol : OrderedFOReduction SAT ThreeCol.

The order is genuinely needed: the OR-gadget chain of a clause is threaded along the order of its literal occurrences (“first occurrence”, “immediate predecessor” and “last occurrence” are FO(≤)-definable, but not FO-definable). This is the standard situation in descriptive complexity, where reductions operate on ordered finite structures.

The file assembles the edge formulas edgeF mirroring SatToCol.Core from the shared occurrence formula builders of DescriptiveComplexity.OccurrenceFormulas (occF, minOccF, succOccF…), and packages everything into the interpretation SatToCol.satToCol and the final reduction.

The edge formulas and the interpretation #

source
noncomputable def DescriptiveComplexity.SatToCol.edgeF :
SatTag → SatTag → SatOcc.satOrd.Formula (Fin 2 × Fin 2)

One direction of the edge formulas of the gadget graph, mirroring SatToCol.Core: the free variable (i, j) is the j-th component of the i-th vertex.

Equations
Instances For
    Dependency graph
    source
    def DescriptiveComplexity.SatToCol.swapVar :
    Fin 2 × Fin 2 → Fin 2 × Fin 2

    Variable swap exchanging the two vertex positions.

    Equations
    Instances For
      Dependency graph
      source
      noncomputable def DescriptiveComplexity.SatToCol.satToCol :
      FOInterpretation SatOcc.satOrd FirstOrder.Language.graph SatTag 2

      The interpretation producing, from an ordered CNF structure, its 3-colorability gadget graph.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Dependency graph
        source
        theorem DescriptiveComplexity.SatToCol.realize_edgeF {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {t₁ t₂ : SatTag} {v : Fin 2 × Fin 2 → A} :
        (edgeF t₁ t₂).Realize v ↔ Core t₁ (v (0, 0)) (v (0, 1)) t₂ (v (1, 0)) (v (1, 1))
        Dependency graph
        source
        theorem DescriptiveComplexity.SatToCol.relMap_adj_iff {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {t₁ t₂ : SatTag} {w₁ w₂ : Fin 2 → A} :
        FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![(t₁, w₁), (t₂, w₂)] ↔ Core t₁ (w₁ 0) (w₁ 1) t₂ (w₂ 0) (w₂ 1) ∨ Core t₂ (w₂ 0) (w₂ 1) t₁ (w₁ 0) (w₁ 1)

        Characterization of the interpreted adjacency relation: it is the symmetrization of Core.

        Dependency graph

        Main theorem #

        source
        theorem DescriptiveComplexity.SatToCol.satisfiable_iff_threeColorable (A : Type) [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] :
        Satisfiable A ↔ ThreeColorable (satToCol.Map A)

        Correctness of the reduction: an ordered CNF structure is satisfiable iff its interpreted gadget graph is 3-colorable.

        Dependency graph
        source
        noncomputable def DescriptiveComplexity.sat_ordered_fo_reduction_threeCol :
        OrderedFOReduction SAT ThreeCol

        SAT FO-reduces to 3-colorability on ordered structures. The reverse fo_reduction theorem: the first-order interpretation SatToCol.satToCol, over the ordered expansion of the language of CNF instances, maps a finite CNF structure to a 3-colorable graph iff it is satisfiable. Together with threeCol_fo_reduction_sat, SAT and 3-colorability are FO-interreducible.

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