Replace a finite many-variable relation R(X1,…,Xk) by one auxiliary variableY whose domain is the allowed tuples of R, together with binary constraints equating each tuple coordinate to its corresponding Xi. Any original satisfying assignment extends to exactly its allowed tuple, and any satisfying encoded assignment projects to a solution of R. The tuple domain can be large; the transformation changes arity, not necessarily representation size efficiently when R is succinct.
