Solution (source code)

= Solution

Let $Q=\{1,\ldots,n\}^2$ be the board squares and let $\operatorname{Attack}(p,q)$ mean that the absolute coordinate differences are $(1,2)$ or $(2,1)$.

\b[One <variable> per knight.] Use $X_1,\ldots,X_k$, with each <constraint domain> equal to $Q$. For every pair $i<j$, require
$$
X_i\ne X_j,\qquad\neg\operatorname{Attack}(X_i,X_j).
$$
Every satisfying assignment places $k$ distinct nonattacking knights, and any such placement gives an assignment after labelling its knights. This has only $k$ <variables> and $O(k^2)$ <binary constraints>, but domains of size $n^2$. Relabelling the knights gives $k!$ assignments for the same unlabelled board, so the representation contains considerable redundancy.

\b[One <Boolean variable> per square.] Use $Y_q\in\{0,1\}$ for every $q\in Q$. Impose the <cardinality constraint>
$$
\sum_{q\in Q}Y_q=k,
$$
and for every knight-attack pair $p,q$ impose $Y_p+Y_q\leq1$. There are $n^2$ <variables>, each with a two-element <constraint domain>, and only $O(n^2)$ local attack restrictions, because each square attacks at most eight others. The single counting constraint is a global constraint, not a <binary constraint>.

The square encoding avoids knight-label redundancy and has sparse local attack relations; the knight encoding uses fewer <variables> when $k$ is small and makes single-knight moves natural. Both are exact representations of the <nonattacking knights problem>. Neither may impose one knight per row: several knights can legally share a row.