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.

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

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

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

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

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

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

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

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.

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

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

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.

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.

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.