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\).