Documentation

DescriptiveComplexity.Problems.ThreeColorability.ToSat

3-colorability FO-reduces to SAT #

This file constructs a (quantifier-free) first-order reduction from graph 3-colorability to CNF satisfiability, DescriptiveComplexity.threeCol_fo_reduction_sat : FOReduction ThreeCol SAT, formalizing the classical encoding used by SAT solvers:

for every vertex u and color i < 3, a propositional variable xᵤᵢ (“u gets color i”), represented by the element (varC i, ![u, u]);
for every vertex u, a clause xᵤ₀ ∨ xᵤ₁ ∨ xᵤ₂, represented by (vtxClause, ![u, u]);
for every edge (u, v) and color i, a clause ¬xᵤᵢ ∨ ¬xᵥᵢ, represented by (edgClause i, ![u, v]).

The resulting CNF is satisfiable iff the graph is 3-colorable (DescriptiveComplexity.threeColorable_iff_satisfiable); note that the usual “at most one color per vertex” clauses are not needed for the equivalence. All defining formulas are quantifier-free (DescriptiveComplexity.threeColToSat_isQuantifierFree), so this is even a quantifier-free reduction, the weakest reduction notion in common use in descriptive complexity.

Elements of the interpreted universe not of the shapes above (“junk”, e.g. (varC i, ![u, v]) with u ≠ v, or (edgClause i, ![u, v]) with (u, v) not an edge) are neither clauses nor occur in any clause, so they do not affect satisfiability.

inductive DescriptiveComplexity.ColTag :

Tags for the tagged 2-dimensional interpretation of SAT instances in graphs.

varC : Fin 3 → ColTag
(varC i, ![u, u]) is the propositional variable “u gets color i”.
vtxClause : ColTag
(vtxClause, ![u, u]) is the clause “u gets some color”.
edgClause : Fin 3 → ColTag
(edgClause i, ![u, v]) is the clause “u and v do not both get color i” (present when (u, v) is an edge).

Instances For

Dependency graph

def DescriptiveComplexity.instDecidableEqColTag.decEq (x✝ x✝¹ : ColTag) :

Decidable (x✝ = x✝¹)

Equations

Instances For

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.instDecidableEqColTag :

DecidableEq ColTag

Equations

DescriptiveComplexity.instDecidableEqColTag = DescriptiveComplexity.instDecidableEqColTag.decEq

Dependency graph

@[instance_reducible]

instance DescriptiveComplexity.instFintypeColTag :

Equations

DescriptiveComplexity.instFintypeColTag = Fintype.ofEquiv (Fin 3 ⊕ Unit ⊕ Fin 3) DescriptiveComplexity.ColTag.proxyTypeEquiv

Dependency graph

instance DescriptiveComplexity.instNonemptyColTag :

Nonempty ColTag

Dependency graph

def DescriptiveComplexity.isClauseFormula :

ColTag → FirstOrder.Language.graph.Formula (Fin 1 × Fin 2)

Defining formula for satIsClause: vertex clauses are the diagonal vtxClause-elements, edge clauses for color i are the edgClause i-elements carrying an edge.

Equations

Instances For

Dependency graph

def DescriptiveComplexity.posInFormula :

ColTag → ColTag → FirstOrder.Language.graph.Formula (Fin 2 × Fin 2)

Defining formula for satPosIn: the vertex clause of u contains positively exactly the variables xᵤᵢ.

Equations

One or more equations did not get rendered due to their size.
DescriptiveComplexity.posInFormula x✝¹ x✝ = ⊥

Instances For

Dependency graph

def DescriptiveComplexity.negInFormula :

ColTag → ColTag → FirstOrder.Language.graph.Formula (Fin 2 × Fin 2)

Defining formula for satNegIn: the edge clause of (u, v) for color i contains negatively exactly the variables xᵤᵢ and xᵥᵢ.

Equations

One or more equations did not get rendered due to their size.
DescriptiveComplexity.negInFormula x✝¹ x✝ = ⊥

Instances For

Dependency graph

def DescriptiveComplexity.threeColToSat :

FOInterpretation FirstOrder.Language.graph FirstOrder.Language.sat ColTag 2

The first-order interpretation producing, from a graph, the CNF instance expressing its 3-colorability.

Equations

One or more equations did not get rendered due to their size.

Instances For

Dependency graph

@[simp]

theorem DescriptiveComplexity.isClause_varC {V : Type} [FirstOrder.Language.graph.Structure V] (i : Fin 3) (w : Fin 2 → V) :

¬FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![(ColTag.varC i, w)]

Dependency graph

@[simp]

theorem DescriptiveComplexity.isClause_vtxClause {V : Type} [FirstOrder.Language.graph.Structure V] (w : Fin 2 → V) :

FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![(ColTag.vtxClause , w)] ↔ w 0 = w 1

Dependency graph

@[simp]

theorem DescriptiveComplexity.isClause_edgClause {V : Type} [FirstOrder.Language.graph.Structure V] (i : Fin 3) (w : Fin 2 → V) :

FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![(ColTag.edgClause i, w)] ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![w 0, w 1]

Dependency graph

@[simp]

theorem DescriptiveComplexity.posIn_iff {V : Type} [FirstOrder.Language.graph.Structure V] (tc tx : ColTag) (wc wx : Fin 2 → V) :

FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![(tc, wc), (tx, wx)] ↔ (∃ (i : Fin 3), tc = ColTag.vtxClause ∧ tx = ColTag.varC i) ∧ (wc 0 = wc 1 ∧ wx 0 = wx 1) ∧ wc 0 = wx 0

Dependency graph

@[simp]

theorem DescriptiveComplexity.negIn_iff {V : Type} [FirstOrder.Language.graph.Structure V] (tc tx : ColTag) (wc wx : Fin 2 → V) :

FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![(tc, wc), (tx, wx)] ↔ (∃ (i : Fin 3), tc = ColTag.edgClause i ∧ tx = ColTag.varC i) ∧ (FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![wc 0, wc 1] ∧ wx 0 = wx 1) ∧ (wx 0 = wc 0 ∨ wx 0 = wc 1)

Dependency graph

def DescriptiveComplexity.colAssignment {V : Type} (col : V → Fin 3) :

ColTag × (Fin 2 → V) → Prop

The truth assignment induced by a coloring: xᵤᵢ is true iff u gets color i. (Junk elements are assigned False.)

Equations

Instances For

Dependency graph

@[simp]

theorem DescriptiveComplexity.colAssignment_varC {V : Type} (col : V → Fin 3) (i : Fin 3) (w : Fin 2 → V) :

colAssignment col (ColTag.varC i, w) ↔ col (w 0) = i

Dependency graph

theorem DescriptiveComplexity.threeColorable_iff_satisfiable (V : Type) [FirstOrder.Language.graph.Structure V] :

ThreeColorable V ↔ Satisfiable (threeColToSat.Map V)

Correctness of the reduction: a graph is 3-colorable iff the interpreted CNF instance is satisfiable.

Dependency graph

def DescriptiveComplexity.threeCol_fo_reduction_sat :

FOReduction ThreeCol SAT

3-colorability FO-reduces to SAT. The fo_reduction theorem: the first-order interpretation threeColToSat maps a graph to a satisfiable CNF instance iff the graph is 3-colorable.

Equations

One or more equations did not get rendered due to their size.

Instances For

Dependency graph

theorem DescriptiveComplexity.threeColToSat_isQuantifierFree :

threeColToSat.IsQuantifierFree

The reduction is even quantifier-free.

Dependency graph

theorem DescriptiveComplexity.SimpleGraph.colorable_iff_satisfiable {V : Type} (G : SimpleGraph V) :

G.Colorable 3 ↔ Satisfiable (threeColToSat.Map V)

Corollary in terms of Mathlib's SimpleGraph: a simple graph is 3-colorable iff the CNF instance interpreted in it is satisfiable.

Dependency graph