A three-CNF formula as a fixed-alphabet binary constraint graph

For each old variable add one shared bit vertex. For each clause $C_i$ add a private tuple vertex $z_i$ and put $A_i=\{a\in \{0,1{\}}^3:C_i\text{ evaluates to true on }(a_1,a_2,a_3)\}$. For each occurrence $j=1,2,3$, add a separate edge from $z_i$ to the old variable in ${\mathrm{\ell }}_{ij}$ with relation $S_{ij}=\{(T(a),B(a_j)):a\in A_i\}$. Thus every clause contributes exactly three edges, including parallel edges when variables repeat, for a total of $3m$.

If $F$ is satisfied by an assignment $\sigma$, label each old vertex by $B(\sigma (x))$ and each $z_i$ by the tuple of the three variable values at its occurrences. That tuple lies in $A_i$, so all three edges of every clause star pass and $\mathrm{val}(G_F)=1$.

Conversely, if all graph edges pass, each clause tuple vertex has a label $T(a)$ with $a\in A_i$, and each edge forces its occurrence coordinate to equal the corresponding old bit label. A repeated variable uses the same old vertex on every occurrence edge, so the equalities are consistent. Therefore each original clause is true under the old bit labels; hence $F$ is satisfiable.

The two implications prove $\mathrm{val}(G_F)=1$ exactly when $F$ is satisfiable. If $m=0$, the graph is edgeless, has value one by convention, and the empty conjunction is true. If $m\ge 1$ and $F$ is unsatisfiable, step 2.2 shows no graph labeling can satisfy all $3m$ edges, so every labeling violates at least one and $\mathrm{UNSAT}(G_F)\ge 1\mathrm{/}(3m)$. The alphabet and each edge table have constant size, so the explicit construction is polynomial time.