Discard tautological clauses first. Give each retained clause a tensor that returns one exactly when that clause is satisfied. Use one port per DISTINCT variable in that clause; repeated literals do not create independent occurrences. Connect all ports belonging to one formula variable with a unary (1,1) tensor, a two-port equality, or a three-port equality tree as appropriate. With width bound k, there are at most km clause ports, O_k(n+m) wires and vertices, and maximum degree max(k,3). Every satisfying assignment on occurring variables extends uniquely through the equality trees. Other assignments contribute zero. An empty clause is handled immediately as unsatisfiable.