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

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.

Three-colorability is a constraint satisfaction problem, and its constraints are clauses of at most three literals: a graph is three-colorable exactly when the 3-CNF formula with a variable x(v, c) for each vertex v and color c, a clause x(v, 0) ∨ x(v, 1) ∨ x(v, 2) for each vertex and a clause ¬x(u, c) ∨ ¬x(v, c) for each edge (u, v) and color c is satisfiable. A loop at v gives the clauses ¬x(v, c), making the formula unsatisfiable, as the loop makes the graph uncolorable. This construction is a tagged interpretation (Cslib.Logic.FO.graph.cnfInterpretation), so 3COL, with loops allowed, is order-free reducible to 3SAT (Cslib.Logic.FO.graph.reduces_ThreeColorable_ThreeSAT); with the converse Cslib.Logic.FO.cnf.reduces_ThreeSAT_ThreeColorable, the two classes are order-free interreducible.

Main definitions

• Cslib.Logic.FO.graph.cnfInterpretation: the 3-CNF structure of the colorings of a graph.

Main results

• Cslib.Logic.FO.graph.satisfiable_cnfInterpretation_iff: the structure is satisfiable exactly when the graph is three-colorable, and Cslib.Logic.FO.graph.isThreeCNF_cnfInterpretation: it is a 3-CNF structure.
• Cslib.Logic.FO.graph.reduces_ThreeColorable_ThreeSAT: 3COL is order-free reducible to 3SAT.

References

• M. R. Garey and D. S. Johnson, Computers and Intractability

inductive Cslib.Logic.FO.graph.ColoringClauseTag : Type

The kinds of elements of the CNF structure of the colorings of a graph: the variables x(v, c), the clauses saying that a vertex has a color, and the clauses saying that the two ends of an edge do not both have the color c.

• var (c : Fin 3) : ColoringClauseTag

  The variables x(v, c): the vertex v has the color c.

• vertex : ColoringClauseTag

  The clauses x(v, 0) ∨ x(v, 1) ∨ x(v, 2).

• edge (c : Fin 3) : ColoringClauseTag

  The clauses ¬x(u, c) ∨ ¬x(v, c) of the edges (u, v).

instance Cslib.Logic.FO.graph.instFiniteColoringClauseTag : Finite ColoringClauseTag

@[reducible, inline]

abbrev Cslib.Logic.FO.graph.ColoringClauseTag.Coord : ColoringClauseTag → Type

The coordinates of the elements: the vertex of a variable or of a vertex clause, and the two ends of the edge of an edge clause.

instance Cslib.Logic.FO.graph.instFiniteColoringClauseTagCoord (t : ColoringClauseTag) : Finite t.Coord

def Cslib.Logic.FO.graph.coloringClauseTemplates (t : ColoringClauseTag) : Bool → List (TaggedInterpretation.Template FirstOrder.Language.graph ColoringClauseTag.Coord t)

The templates of the literals of each polarity. A variable names the tautology x ∨ ¬x.

noncomputable def Cslib.Logic.FO.graph.cnfInterpretation : TaggedInterpretation FirstOrder.Language.graph cnf ColoringClauseTag ColoringClauseTag.Coord

The CNF structure of the colorings of a graph, a tagged interpretation.

theorem Cslib.Logic.FO.graph.satisfiable_cnfInterpretation_iff {M : Type u_1} [FirstOrder.Language.graph.Structure M] : cnf.Satisfiable (cnfInterpretation.Model M) ↔ Colorable 3 M

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

theorem Cslib.Logic.FO.graph.isThreeCNF_cnfInterpretation {M : Type u_1} [FirstOrder.Language.graph.Structure M] : cnf.IsThreeCNF (cnfInterpretation.Model M)

The CNF structure of the colorings of a graph is a 3-CNF structure.

Structures with at most one element

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

On a graph with at most one vertex: a single clause, the clause x without a loop and the empty clause with a loop.

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

3COL reduces to 3SAT by an order-free first-order interpretation.