TAOCP 7.2.2.2 Exercise 13
Let $p_{k,i}$ denote the choice of placing the first occurrence of $k\in\{1,2,3,4\}$ at position $i$ in a length $8$ sequence, with the second occurrence forced to lie at position $i+k+1$.
Section 7.2.2.2: Satisfiability
Exercise 13. [24] [24] Exercise 7.2.2.1–00 defines an exact cover problem that corresponds to Langford pairs of order $n$. (See page vii.)
a) What are the constraints analogous to (12) when $n = 4$? b) Show that there's a simple way to avoid duplicate binary clauses such as those in (14), whenever an exact cover problem is converted to clauses using (13). c) Describe the corresponding clauses $\textit{langford}(4)$ and $\textit{langford}'(4)$.
Verified: yes
Solve time: 2m24s
(a) Constraints analogous to (12) for $n=4$
Let $p_{k,i}$ denote the choice of placing the first occurrence of $k\in{1,2,3,4}$ at position $i$ in a length $8$ sequence, with the second occurrence forced to lie at position $i+k+1$. This placement is admissible exactly when $i+k+1\le 8$, i.e. $i\in I_k$ where
$$ I_1={1,2,3,4,5,6},\quad I_2={1,2,3,4,5},\quad I_3={1,2,3,4},\quad I_4={1,2,3}. $$
The exact cover formulation underlying (12) requires two kinds of constraints.
First, each value $k$ must be used exactly once. This is expressed by requiring that among all admissible placements of $k$, exactly one is chosen. In CNF form this becomes an “at least one” clause together with pairwise exclusion:
$$ \bigvee_{i\in I_k} p_{k,i}, \qquad \neg p_{k,i}\vee \neg p_{k,i'} \ \text{for } i\ne i',\ i,i'\in I_k, \qquad k=1,2,3,4. $$
Second, each position $j\in{1,\dots,8}$ must be covered exactly once. Let
$$ A_j={(k,i)\mid j=i \text{ or } j=i+k+1}. $$
Then each position constraint consists of
$$ \bigvee_{(k,i)\in A_j} p_{k,i}, \qquad \neg p_{k,i}\vee \neg p_{k',i'} \ \text{for distinct } (k,i),(k',i')\in A_j, \qquad j=1,\dots,8. $$
Together these express that every number is placed once and every position is covered exactly once, matching the exact cover constraints in (12).
(b) Avoiding duplicate binary clauses in the translation of (13)
In the standard exact cover to CNF translation (13), a binary clause $\neg x\vee \neg y$ is produced for each pair of distinct rows that overlap in a column. A potential source of duplication would be the same pair of rows being generated from more than one column.
In the Langford encoding, each placement $p_{k,i}$ covers exactly two positions, namely $i$ and $i+k+1$. Therefore any two distinct placements can intersect in at most one position. Indeed, if two placements agreed on two different positions, they would coincide completely, contradicting distinctness.
Hence, for any incompatible pair $(k,i)\neq (k',i')$, there is at most one position $j$ such that both belong to $A_j$. It follows that the pair can arise in at most one column constraint.
Therefore the translation (13) already generates each binary clause $\neg p_{k,i}\vee \neg p_{k',i'}$ at most once. No canonical tie-breaking rule is needed, because the overlap structure of Langford placements prevents multi-column duplication.
A simple way to avoid duplicates, if one insists on implementing (13) mechanically, is to store generated clauses in a set keyed by unordered pairs ${(k,i),(k',i')}$. In this specific problem this has no mathematical effect beyond implementation hygiene, since no duplicates actually occur.
(c) The clauses $\mathrm{langford}(4)$ and $\mathrm{langford}'(4)$
The formula $\mathrm{langford}(4)$ consists of all clauses produced by the exact cover encoding:
For each $k\in{1,2,3,4}$, a clause ensuring that one admissible placement of $k$ is chosen,
$$ \bigvee_{i\in I_k} p_{k,i}, $$
together with all pairwise exclusions within the same $k$,
$$ \neg p_{k,i}\vee \neg p_{k,i'} \quad (i\ne i'). $$
For each position $j\in{1,\dots,8}$, a clause ensuring coverage,
$$ \bigvee_{(k,i)\in A_j} p_{k,i}, $$
together with all pairwise exclusions between distinct placements in $A_j$,
$$ \neg p_{k,i}\vee \neg p_{k',i'} \quad \text{for distinct } (k,i),(k',i')\in A_j. $$
From part (b), no binary clause is ever generated more than once by different position constraints. Therefore the reduced formula $\mathrm{langford}'(4)$, obtained by removing duplicate clauses if any arise during mechanical construction, coincides exactly with $\mathrm{langford}(4)$. That is,
$$ \mathrm{langford}'(4)=\mathrm{langford}(4). $$
The distinction between the two formulas is therefore purely procedural rather than structural in this instance, since the Langford $n=4$ instance does not produce repeated binary clauses under the standard exact-cover translation.