TAOCP 7.2.2.2 Exercise 518
In the direct encoding, each variable $x_i$ is represented by Boolean variables indicating its possible values.
Section 7.2.2.2: Satisfiability
Exercise 518. [M32] [M32] Given a 3SAT problem with $m$ clauses and $n$ variables, we shall construct a $(6m + n) \times (6m + n)$ matrix $M$ of integers such that the permanent, per $M$, is zero if and only if the clauses are unsatisfiable. For example, the solvable problem (7) corresponds to the $46 \times 46$ matrix indicated here; each shaded box stands for a fixed $A$ submatrix of $A$ that corresponds to a clause.
Each $A$ has three "inputs" in columns 1, 3, 5 and three "outputs" in rows 2, 4, 6. The first $n$ rows and the last $n$ columns correspond to variables. Outside of the $A$s, all entries are either 0 or 2; and the 2s link variables to clauses, according to a scheme much like the data structures in several of the algorithms in this section: Let $I_{ij}$ and $O_{ij}$ denote the $j$th input and output of clause $i$, for $1 \le i \le m$ and $1 \le j \le 3$. Then, if literal $l$ appears in $t \ge 0$ clauses $i_1 < \cdots < i_t$, its elements $j_1, \ldots, j_t$, we put '2' in column $I_{i_k j_k}$ of row $O_{i_k j_k}$ for $0 \le k \le t$ (if $O_{i_0 j_0}$ is row $|l|$, $I_{i_{t+1} j_{t+1}}$ is column $|l|$).

a) Find a $6 \times 6$ matrix $A = (a_{ij})$, whose elements are either 0, 1, or $-1$, such that
$$\operatorname{per}\begin{pmatrix} a_{11} & a_{12} & a_{13} & a_{14} & a_{15} & a_{16} \ a_{21}+2r & a_{22} & a_{23}+2s & a_{24} & a_{25}+2t & a_{26} \ a_{31} & a_{32} & a_{33} & a_{34} & a_{35} & a_{36} \ a_{41}+2u & a_{42} & a_{43}+2v & a_{44} & a_{45}+2w & a_{46} \ a_{51} & a_{52} & a_{53} & a_{54} & a_{55} & a_{56} \ a_{61}+2x & a_{62} & a_{63}+2y & a_{64} & a_{65}+2z & a_{66} \end{pmatrix} = 16!\left(\operatorname{per}\begin{pmatrix} r+1 & s & t \ u & v+1 & w \ x & y & z+1 \end{pmatrix} - 1\right)$$
Hint: There's a solution with lots of symmetry.
b) In which of the rows and columns of $M$ does '2' occur twice? once? not at all?
c) Conclude that $\operatorname{per} M = 2^{4m+n} s$, where the problem has exactly $s$ solutions.
Verified: no
Solve time: 3m47s
Solution
In the direct encoding, each variable $x_i$ is represented by Boolean variables indicating its possible values. Write
$$ x_{i,j}=1\iff x_i=j, $$
where $0\le i<p$ and $1\le j\le d$ if the domain has size $d$. The direct encoding already contains the clauses forcing each $x_i$ to have exactly one value. The all-different constraint adds the requirement that two different variables cannot choose the same value.
For two distinct variables $x_i$ and $x_k$, and for any value $j$, the assignment
$$ x_{i,j}=x_{k,j}=1 $$
must be forbidden. The corresponding clause is
$$ \bar{x}{i,j}\vee \bar{x}{k,j}. $$
Taking all pairs of variables and all possible values gives the complete encoding:
$$ \bigwedge_{0\le i<k<p}\ \bigwedge_{1\le j\le d} (\bar{x}{i,j}\vee\bar{x}{k,j}). $$
These clauses are sufficient. Suppose the direct variables represent an assignment satisfying the clauses. If two variables $x_i$ and $x_k$ had the same value $j$, then the direct encoding would require
$$ x_{i,j}=1,\qquad x_{k,j}=1. $$
The clause
$$ \bar{x}{i,j}\vee\bar{x}{k,j} $$
would then be false, contradicting satisfiability. Hence no two variables receive the same value.
They are also necessary. Given any assignment satisfying the all-different constraint, no pair of variables $x_i,x_k$ has the same value. Therefore, for every $j$, at least one of $x_{i,j}$ and $x_{k,j}$ is false, so every clause
$$ \bar{x}{i,j}\vee\bar{x}{k,j} $$
is satisfied.
Thus the all-different constraint in the direct encoding is enforced by adding one binary clause for every pair of variables and every possible value:
$$ \boxed{\bar{x}{i,j}\vee\bar{x}{k,j}\qquad (0\le i<k<p,\ 1\le j\le d).} $$
This completes the proof. ∎