 Nonattacking knights problem

Choose $k$ distinct squares of an $n\times n$ chessboard so that no chosen pair has absolute coordinate differences $(1,2)$ or $(2,1)$. One constraint satisfaction problem representation has $k$ square-valued variables, requiring distinctness and pairwise nonattack. Another has one Boolean variable per square, a cardinality constraint fixing their sum to $k$, and one mutual-exclusion constraint for every edge of the knight attack graph. The first has fewer variables when $k$ is small but represents each unlabelled placement up to $k!$ times; the second uses only binary constraint domains and sparse local attack restrictions.