The order-free first-order interpretation from 3SAT to 3COL

The reductions in this module use order-free first-order interpretations. Input structures have no built-in order or numeric predicates; these are variants of the standard ordered setting.

The palette, variable and clause gadget reduction from 3SAT to three-colorability, a standard exercise Sipser, Chapter 7 (three-colorability is NP-complete Garey and Johnson), is first-order on CNF structures (Cslib.Logic.FO.cnf.reduces_ThreeSAT_ThreeColorable). From a 3-CNF structure it builds a palette triangle T, F, B, two literal vertices x and ¬x for each variable, joined to each other and to B, and for each clause a gadget of six vertices, two chained OR gates whose output is joined to F and B. A clause with at most three literals has no canonical order, so there is a gadget for every triple of its literals that lists all of them; each such gadget forces the clause. The construction is a tagged interpretation, the tags being the kinds of vertices. Inputs that are not 3-CNF structures, or that have an empty clause, are mapped to graphs with a loop.

The target is the class graph.ThreeColorable of three-colorable graph structures, loops allowed. On the members of 3SAT the graph is symmetric and loopless, so the same interpretation reduces 3SAT to classical three-colorability of simple graphs (Cslib.Logic.FO.cnf.reduces_ThreeSAT_SimpleThreeColorable). The machine-level reduction, on encoded formulas and graphs, is Cslib.Complexity.SAT.toThreeColoring.

Main definitions

• Cslib.Logic.FO.cnf.coloringInterpretation: the graph built from a CNF structure, a tagged interpretation.

Main results

• Cslib.Logic.FO.cnf.colorable_coloringInterpretation_iff: the graph built from a CNF structure is three-colorable exactly when the structure is a satisfiable 3-CNF structure.
• Cslib.Logic.FO.cnf.reduces_ThreeSAT_ThreeColorable, Cslib.Logic.FO.cnf.reduces_ThreeSAT_SimpleThreeColorable: 3SAT is order-free reducible to 3COL, with loops allowed or on simple graphs.

References

• M. Sipser, Introduction to the Theory of Computation
• M. R. Garey and D. S. Johnson, Computers and Intractability
• N. Immerman, Descriptive Complexity

The clause gadget

def Cslib.Logic.FO.cnf.orGate (u v : Fin 3) : Fin 3 × Fin 3 × Fin 3

An OR gate on colors, with true 0, false 1 and base 2: the colors of the vertices adjacent to the two inputs and of the output.

def Cslib.Logic.FO.cnf.gadgetColor (u v w : Fin 3) : Fin 6 → Fin 3

The coloring of the six vertices of the clause gadget for inputs colored u, v, w.

@[reducible, inline]

abbrev Cslib.Logic.FO.cnf.GadgetProper (u v w : Fin 3) (g : Fin 6 → Fin 3) (f b : Fin 3) : Prop

The edges of the clause gadget with inputs u, v, w and palette t, f, b are properly colored by g: vertices 0, 1, 2 and 3, 4, 5 are triangles, 0 is joined to u, 1 to v, 2 to 3, 4 to w, and 5 to f and b.

The graph of a CNF structure

inductive Cslib.Logic.FO.cnf.ColoringTag : Type

The kinds of vertices of the graph built from a CNF structure: the palette T, F, B, the literal vertices of each polarity, and the vertices of the clause gadgets, for each pattern of polarities of the three literals of the gadget.

• trueV : ColoringTag

  The palette vertex of true.

• falseV : ColoringTag

  The palette vertex of false.

• baseV : ColoringTag

  The palette vertex joined to all literals.

• lit (p : Bool) : ColoringTag

  The literal vertices of a polarity.

• gadget (g : Fin 6) (ps : Fin 3 → Bool) : ColoringTag

  The vertex g of the gadgets of a pattern of polarities.

instance Cslib.Logic.FO.cnf.instFiniteColoringTag : Finite ColoringTag

@[reducible, inline]

abbrev Cslib.Logic.FO.cnf.ColoringTag.Coord : ColoringTag → Type

The coordinates of the vertices: none for the palette, the variable of a literal vertex, and the clause and the three literal variables of a gadget vertex.

instance Cslib.Logic.FO.cnf.instFiniteColoringTagCoord (u : ColoringTag) : Finite u.Coord

def Cslib.Logic.FO.cnf.GadgetDomain {M : Type u_1} [cnf.Structure M] (ps : Fin 3 → Bool) (d : Fin 4 → M) : Prop

A gadget with coordinates d lists the literals (ps i, d (i + 1)) of the clause d 0, and all of them.

noncomputable def Cslib.Logic.FO.cnf.gadgetDomain (ps : Fin 3 → Bool) : cnf.Formula (Fin 4)

The domain formula of the gadgets of a pattern of polarities.

noncomputable def Cslib.Logic.FO.cnf.badSentence : cnf.Sentence

The sentence saying that the structure is not a 3-CNF structure with nonempty clauses.

noncomputable def Cslib.Logic.FO.cnf.coloringEdges (u : ColoringTag) : List (TaggedInterpretation.Template cnf ColoringTag.Coord u)

The edges of the graph, from each kind of vertex: the palette triangle, with a loop at T on bad inputs, the literal vertices joined to B and x joined to ¬x, and the gadgets.

noncomputable def Cslib.Logic.FO.cnf.coloringAdj (u w : ColoringTag) : cnf.Formula (u.Coord ⊕ w.Coord)

The formula of the edges between vertices of kinds u and w, in both directions.

noncomputable def Cslib.Logic.FO.cnf.coloringInterpretation : TaggedInterpretation cnf FirstOrder.Language.graph ColoringTag ColoringTag.Coord

The graph of a CNF structure, a tagged interpretation: the edges are those of coloringEdges, in both directions.

Correctness

theorem Cslib.Logic.FO.cnf.colorable_coloringInterpretation_iff {M : Type u_1} [cnf.Structure M] : graph.Colorable 3 (coloringInterpretation.Model M) ↔ IsThreeCNF M ∧ Satisfiable M

The graph of a CNF structure is three-colorable exactly when the structure is a satisfiable 3-CNF structure.

theorem Cslib.Logic.FO.cnf.simpleGraph_coloringInterpretation {M : Type u_1} [cnf.Structure M] (h3 : IsThreeCNF M) (hne : ∀ (c : M), (literals c).Nonempty) : coloringInterpretation.Model M ⊨ FirstOrder.Language.Theory.simpleGraph

On a 3-CNF structure without empty clauses, the graph is a simple graph.

Structures with at most one element

def Cslib.Logic.FO.cnf.coloringSubsingleton : Interpretation cnf FirstOrder.Language.graph Unit

On a structure with at most one element: a single vertex, with a loop when its clause is empty.

theorem Cslib.Logic.FO.cnf.reduces_ThreeSAT_ThreeColorable : Reduces ThreeSAT graph.ThreeColorable

3SAT is order-free reducible to 3COL, by the palette, variable and clause gadget construction Sipser, Chapter 7, Immerman, Chapter 7.

theorem Cslib.Logic.FO.cnf.reduces_ThreeSAT_SimpleThreeColorable : Reduces ThreeSAT graph.SimpleThreeColorable

3SAT is order-free reducible to classical 3COL, three-colorability of simple graphs: on the members of 3SAT the graph of the reduction is symmetric and loopless.