90 Complexity — NAESAT To Coloring
90.1 Overview
This module formalises the polynomial-time reduction from Not-All-Equal 3-SAT (NAE-SAT) to 3-Coloring. Given a NAE-SAT instance over Boolean variables \(x_1,\dots ,x_n\) and clauses \(C_1,\dots ,C_m\), it constructs an explicit simple graph whose 3-colorability is equivalent to the satisfiability of the instance, and proves both completeness and soundness of that correspondence.
90.2 Declarations
Given a Boolean assignment \(\mathit{assign} : V \to \mathtt{Bool}\) and a Not-All-Equal clause \(c\) with three variables \(c.v_0, c.v_1, c.v_2\), \(\texttt{NAEtoColor.SatisfiesClause}\) returns \(\mathtt{true}\) if and only if the three assigned values are not all equal, i.e. at least two of \(\mathit{assign}(c.v_0)\), \(\mathit{assign}(c.v_1)\), \(\mathit{assign}(c.v_2)\) differ.
A NAE-SAT instance over variable type \(V\) is defined as a list of NAE clauses, i.e. \(\texttt{NAEtoColor.NAESat3}\; V = \mathtt{List}\; (\mathtt{NAEclause}\; V)\).
Given an assignment \(\mathit{assign} : V \to \mathtt{Bool}\) and a NAE-SAT instance \(f\), \(\texttt{NAEtoColor.SatisfiesNAE3}\) returns \(\mathtt{true}\) if and only if every clause in \(f\) is satisfied by \(\mathit{assign}\) (i.e. \(\texttt{NAEtoColor.SatisfiesClause}\) holds for each clause).
A NAE-SAT instance \(f\) over variable type \(V\) is satisfiable if there exists a Boolean assignment \(\mathit{assign} : V \to \mathtt{Bool}\) such that \(\texttt{NAEtoColor.SatisfiesNAE3}\; \mathit{assign}\; f = \mathtt{true}\).
A concrete NAE-SAT instance over \(\mathrm{Fin}\, 5\) consisting of three clauses: \(\langle 0,1,2\rangle \), \(\langle 0,1,3\rangle \), \(\langle 0,2,4\rangle \).
A concrete Boolean assignment for \(\mathrm{Fin}\, 5\) given by \(\! [{\mathtt{true}},{\mathtt{true}},{\mathtt{false}},{\mathtt{false}},{\mathtt{false}}]\), which witnesses satisfiability of NAEtoColor.NAE_SAT_Example.nae_sat_eg.
A simple graph \(G\) on vertex type \(V'\) is 3-colorable if there exists a proper coloring \(G.\mathtt{Coloring}\; (\mathrm{Fin}\, 3)\), i.e. a map from vertices to \(\{ 0,1,2\} \) such that no two adjacent vertices share the same color.
The vertex set of the reduction graph is an inductive type with three constructors:
\(\mathtt{groundNode}\) — a single ground vertex (colored “neutral”);
\(\mathtt{varNode}\; v\) — one vertex per variable \(v \in V\);
\(\mathtt{clauseNode}\; c\; k\) — three internal gadget vertices (\(k \in \mathrm{Fin}\, 3\)) for each clause \(c\).
Given a NAE-SAT instance \(\mathit{clauses}\), the directed edge relation on \(\texttt{NAEtoColor.OutputVertex}\; V\) is defined by: (1) \(\mathtt{groundNode}\) is adjacent to every \(\mathtt{varNode}\); (2) \(\mathtt{varNode}\; v\) is adjacent to \(\mathtt{clauseNode}\; c\; i\) when \(v\) is the \(i\)-th variable of clause \(c\); (3) two clause-gadget nodes \(\mathtt{clauseNode}\; c\; i\) and \(\mathtt{clauseNode}\; c\; j\) are adjacent when \(c \in \mathit{clauses}\) and \(i \neq j\) (forming a triangle within each clause gadget). All other pairs are non-adjacent.
Given a NAE-SAT instance \(f\), \(\texttt{NAEtoColor.ReductionGraph}\; f\) is the simple graph on \(\texttt{NAEtoColor.OutputVertex}\; V\) whose adjacency is the symmetrization of \(\texttt{NAEtoColor.EdgeRelation}\; f\) restricted to distinct pairs (no self-loops).
Given three Boolean values \(a, b, c\) (the truth values of a clause’s three literals) and an index \(k \in \mathrm{Fin}\, 3\), returns the color in \(\mathrm{Fin}\, 3\) assigned to the \(k\)-th internal clause-gadget node. The coloring is chosen so that all three gadget nodes receive distinct colors whenever \((a, b, c)\) is a NAE-satisfying assignment; if the assignment is not NAE-satisfying, all gadget nodes are colored \(0\).
Given a Boolean assignment \(\mathit{assign} : V \to \mathtt{Bool}\), defines a coloring of all vertices of the reduction graph by: \(\mathtt{groundNode} \mapsto 0\); \(\mathtt{varNode}\; v \mapsto 1\) if \(\mathit{assign}(v) = \mathtt{true}\), else \(2\); \(\mathtt{clauseNode}\; c\; k \mapsto \texttt{NAEtoColor.clauseNodeColor}\; (\mathit{assign}(c.v_0))\; (\mathit{assign}(c.v_1))\; (\mathit{assign}(c.v_2))\; k\).
Let \(f\) be a NAE-SAT instance over a variable type \(V\), that is, a list of not-all-equal clauses each naming three variables. If \(f\) is satisfiable — some Boolean assignment \(V \to \{ \mathrm{true}, \mathrm{false}\} \) makes the three variables of every clause not all receive the same value — then the reduction graph of \(f\) is 3-colorable, meaning it admits a proper coloring with the three colors \(\{ 0, 1, 2\} \).
Let \(f\) be a NAE-SAT instance over a variable type \(V\), that is, a list of Not-All-Equal clauses, each clause naming three variables. Form the reduction graph associated to \(f\): its vertices are a single ground vertex, one vertex for each variable in \(V\), and, for every clause, three gadget vertices; its edges join the ground vertex to each variable vertex, join each variable vertex \(v\) to a clause-gadget vertex whenever \(v\) occurs in the corresponding position of that clause, and, for every clause of \(f\), join its three gadget vertices pairwise into a triangle. If this graph is 3-colorable — that is, its vertices admit a coloring by \(\{ 0,1,2\} \) in which adjacent vertices receive distinct colors — then \(f\) is satisfiable: there exists a Boolean assignment \(\mathit{assign} : V \to \{ \mathrm{true},\mathrm{false}\} \) under which every clause of \(f\) has its three assigned values not all equal.
Let \(f\) be a NAE-SAT instance over a variable type \(V\), and let \(\Gamma (f)\) denote its reduction graph, the simple graph built from \(f\) as described above (a ground vertex joined to every variable vertex, each variable vertex joined to the clause-gadget vertices for the clauses in which it occurs, and the three gadget vertices of each clause joined pairwise into a triangle). Then \(f\) is satisfiable if and only if \(\Gamma (f)\) is 3-colorable.
90.3 Additional declarations
A Not-All-Equal clause over a variable type \(V\) is an ordered triple \((v_0, v_1, v_2)\) of variables from \(V\). It records the three variables of one NAE constraint; such a clause is meant to be satisfied by a Boolean assignment exactly when the values assigned to \(v_0\), \(v_1\), \(v_2\) are not all equal.