93 Complexity — Three SAT To Coloring

93.1 Overview

This module formalises the classical polynomial-time reduction from 3-SAT to 3-Coloring. Given a 3-SAT instance over Boolean variables, a gadget graph is constructed whose vertices are palette nodes, literal nodes, and six-node clause gadgets; the main result (SATtoColor.SATtoColorReduction) states that the formula is satisfiable if and only if the reduction graph admits a proper 3-coloring.

93.2 Declarations

Definition 93.1 Clause

✓

A clause over a variable type $V$ is a structure bundling exactly three literals $\ell _1, \ell _2, \ell _3 : \mathrm{Literal}\, V$. Each literal is either a positive or a negative occurrence of some variable.

Definition 93.2 Literal satisfaction

✓

Given a Boolean assignment $\mathrm{assign} : V \to \mathrm{Bool}$, the function $\texttt{SATtoColor.SatisfiesLiteral}$ evaluates a literal: a positive literal $\mathrm{pos}(v)$ evaluates to $\mathrm{assign}(v)$, and a negative literal $\mathrm{neg}(v)$ evaluates to $\neg \, \mathrm{assign}(v)$.

Definition 93.3 Clause satisfaction

✓

Under assignment $\mathrm{assign}$, a clause $c$ is satisfied if at least one of its three literals evaluates to true:

\[ \mathrm{SatisfiesClause}(\mathrm{assign}, c) \; =\; \mathrm{SatisfiesLiteral}(\mathrm{assign}, c.\ell _1) \; \vee \; \mathrm{SatisfiesLiteral}(\mathrm{assign}, c.\ell _2) \; \vee \; \mathrm{SatisfiesLiteral}(\mathrm{assign}, c.\ell _3). \]

Definition 93.4 3-SAT instance

✓

A 3-SAT instance over variable type $V$ is defined as a list of clauses, i.e. $\mathrm{Sat3}(V) := \mathrm{List}(\mathrm{Clause}\, V)$.

Definition 93.5 Simultaneous clause satisfaction

✓

An assignment $\mathrm{assign}$ satisfies a 3-SAT instance $f$ if every clause in the list $f$ is satisfied by $\mathrm{assign}$, i.e. $\mathrm{SatisfiesSat3}(\mathrm{assign}, f) = \texttt{true}$ iff $\forall c \in f,\; \mathrm{SatisfiesClause}(\mathrm{assign}, c) = \texttt{true}$.

Definition 93.6 Satisfiability

✓

A 3-SAT instance $f$ is satisfiable if there exists a Boolean assignment that satisfies it:

\[ \mathrm{IsSatisfiable}(f) \; :=\; \exists \, \mathrm{assign}: V \to \mathrm{Bool},\; \mathrm{SatisfiesSat3}(\mathrm{assign}, f) = \texttt{true}. \]

Definition 93.7 Concrete 3-SAT example

✓

A specific 3-SAT instance over four Boolean variables $x_0, x_1, x_2, x_3$ ($V = \mathrm{Fin}\, 4$), consisting of three clauses: $(x_0 \vee \neg x_1 \vee \neg x_2)$, $(\neg x_0 \vee x_1 \vee \neg x_2)$, and $(\neg x_0 \vee \neg x_1 \vee \neg x_3)$.

Definition 93.8 Example assignment

✓

A concrete Boolean assignment for the example instance $\texttt{SATtoColor.SAT3\_ Example.sat3\_ inst}$, defined as the vector $[{\tt true},\, {\tt true},\, {\tt false},\, {\tt false}]$ indexed by $\mathrm{Fin}\, 4$.

Definition 93.9 Reduction vertex type

✓

The vertex set of the reduction graph is the inductive type $\mathrm{OutputVertex}(V)$ with three constructors:

$\mathrm{palette}(p)$ for $p : \mathrm{Fin}\, 3$ — the three special palette nodes (Base $= 0$, True $= 1$, False $= 2$) forming a triangle that fixes color semantics;
$\mathrm{literalNode}(\ell )$ — one node per literal over $V$ (positive and negative occurrences are separate nodes);
$\mathrm{clauseGadget}(c, k)$ for $k : \mathrm{Fin}\, 6$ — six internal nodes per clause $c$ encoding the OR constraint.

Definition 93.10 3-colorability

✓

A simple graph $G$ on vertex type $V'$ is 3-colorable if there exists a proper graph coloring with colors $\mathrm{Fin}\, 3$, i.e. $\mathrm{Nonempty}(G.\mathrm{Coloring}(\mathrm{Fin}\, 3))$.

Definition 93.11 Reduction edge relation

✓

$\mathrm{EdgeRelation}(f, u, v)$ defines the (undirected) adjacency structure of the reduction graph. The edges are: all pairs of distinct palette nodes; every literal node to the Base palette node; $\mathrm{pos}(x)$ to $\mathrm{neg}(x)$ for each variable $x$; specific pairs of clause gadget nodes within the same clause (encoding two internal triangles on nodes $\{ 0,1,2\} $ and $\{ 3,4,5\} $ plus the bridge $2$–$3$); each clause’s three literal nodes to gadget nodes $0$, $1$, and $4$ respectively; and gadget node $5$ of every clause to both the Base and the False palette nodes.

Definition 93.12 Reduction graph

✓

Given a 3-SAT instance $f$ over variables $V$, the reduction graph $\mathrm{ReductionGraph}(f)$ is the SimpleGraph on $\mathrm{OutputVertex}(V)$ whose adjacency relation is the symmetrisation of $\mathrm{EdgeRelation}(f)$: two distinct vertices are adjacent iff $\mathrm{EdgeRelation}(f, u, v)$ or $\mathrm{EdgeRelation}(f, v, u)$ holds.

Definition 93.13 Clause gadget coloring

✓

Given the Boolean truth values $a, b, c_3$ of the three literals of a clause, $\mathrm{clauseGadgetColor}(a, b, c_3, k)$ assigns a color in $\mathrm{Fin}\, 3$ to gadget node $k \in \{ 0,\ldots ,5\} $. In particular, node $5$ always receives color $1$ (True), and the remaining nodes are colored so that all internal gadget edges receive distinct colors whenever at least one literal is true.

Definition 93.14 Coloring from satisfying assignment

✓

Given a satisfying assignment $\mathrm{assign} : V \to \mathrm{Bool}$, the function $\mathrm{sat3Coloring}(\mathrm{assign})$ maps every vertex of $\mathrm{OutputVertex}(V)$ to a color in $\mathrm{Fin}\, 3$: palette node $p$ gets color $p$; a positive (resp. negative) literal node for variable $v$ gets color $1$ (True) if $\mathrm{assign}(v) = \texttt{true}$ and color $2$ (False) otherwise (resp. the reverse); clause gadget node $(c, k)$ gets $\mathrm{clauseGadgetColor}$ applied to the truth values of $c$’s three literals.

Lemma 93.15 Color of a literal node

✓

Fix a variable type $V$ and a Boolean assignment $\alpha : V \to \{ \text{true}, \text{false}\} $, and consider the coloring of the reduction graph induced by $\alpha $, which sends each vertex to a color in $\{ 0, 1, 2\} $ (with $1$ standing for True and $2$ for False). For every literal $\ell $ over $V$, the literal node of $\ell $ receives color $1$ if $\ell $ is satisfied by $\alpha $, and color $2$ otherwise:

\[ \text{color of the literal node of } \ell \; =\; \begin{cases} 1 & \text{if $\ell $ is satisfied by $\alpha $,}\\ 2 & \text{otherwise.}\end{cases} \]

Lemma 93.16 Completeness of the 3-SAT to 3-coloring reduction

✓

Let $f$ be a 3-SAT instance over a variable type $V$, that is, a list of clauses, each a disjunction of three literals. If $f$ is satisfiable — there exists a Boolean assignment $\mathrm{assign} : V \to \mathrm{Bool}$ under which every clause of $f$ has at least one true literal — then the reduction graph $\mathrm{ReductionGraph}(f)$ is 3-colorable, i.e. it admits a proper coloring by the three colors $\mathrm{Fin}\, 3$.

Lemma 93.17 Soundness of the 3-SAT to 3-colouring reduction

✓

Let $f$ be a 3-SAT instance over a variable type $V$, that is, a list of clauses, each clause a triple of literals (positive or negative occurrences of variables). If the reduction graph $\mathrm{ReductionGraph}(f)$ admits a proper $3$-colouring, then $f$ is satisfiable: there exists a Boolean assignment $\mathrm{assign} \colon V \to \{ \mathrm{true}, \mathrm{false}\} $ under which every clause of $f$ has at least one literal evaluating to $\mathrm{true}$.

Theorem 93.18 Correctness of the 3-SAT to 3-coloring reduction

✓

Let $f$ be a 3-SAT instance over a variable type $V$: a list of clauses, each clause an ordered triple of literals, where a literal is a positive or a negative occurrence of a variable in $V$. Then $f$ is satisfiable — some Boolean assignment $V \to \{ \mathrm{true}, \mathrm{false}\} $ makes every clause in $f$ true — if and only if the reduction graph associated to $f$ is 3-colorable, that is, admits a proper coloring by three colors.

93.3 Additional declarations

Definition 93.19 Literal over a variable type

✓

Given a type $V$ of Boolean variables, a literal over $V$ is either a positive occurrence $\mathrm{pos}(v)$ or a negative occurrence $\mathrm{neg}(v)$ of a variable $v \in V$; a positive literal asserts the variable and a negative literal asserts its negation.