TAOCP 7.2.2.2 Exercise 394
Let $x_{k,j}$ denote the usual Langford variable indicating that the pair of numbers $k,k$ begins in position $j$.
Section 7.2.2.2: Satisfiability
Exercise 394. [25] [25] One way to encode the at-most-one constraint $S_1(y_1 \ldots y_p)$ is to introduce $l = \lfloor \lg p \rfloor$ auxiliary variables together with the following $nd + n - 2^l$ clauses, which essentially "broadcast" the value of $j$ when $y_j$ becomes true:
$$(\bar{y}_j \vee (-1)^{b_t} a_t) \quad \text{for } 1 \le j \le p,\ 1 \le t \le q = \lfloor \lg(2p - j) \rfloor,\ \text{where } 2p - j = (1 b_1 \ldots b_q)_2.$$
For example, the clauses when $p = 3$ are $(\bar{y}_1 \vee \bar{a}_1) \wedge (\bar{y}_1 \vee \bar{a}_2) \wedge (\bar{y}_2 \vee \bar{a}_1) \wedge (\bar{y}_2 \vee a_2) \wedge (\bar{y}_3 \vee \bar{a}_1)$.
Experiment with this encoding by applying it to Langford's problem, using it in place of (12) whenever $p \ge 7$.
Verified: no
Solve time: 2m36s
Solution
Let $x_{k,j}$ denote the usual Langford variable indicating that the pair of numbers $k,k$ begins in position $j$. The constraints in the Langford encoding have two kinds of at-most-one requirements. For each $k$, exactly one starting position must be chosen for the pair $k,k$, and for each position, at most one pair may occupy that position. The clauses expressing these conditions contain instances of $S_1(y_1,\ldots,y_p)$, where the variables $y_i$ are the possible choices for a fixed number or a fixed position.
The encoding of exercise 394 replaces the ordinary pairwise encoding of each $S_1(y_1,\ldots,y_p)$ by a binary encoding with auxiliary variables. Let
$$ l=\lfloor\lg p\rfloor . $$
For every $j$, write
$$ 2p-j=(1b_1\ldots b_q)_2, \qquad q=\lfloor\lg(2p-j)\rfloor . $$
The new clauses are
$$ (\bar y_j\vee (-1)^{b_t}a_t), \qquad 1\le j\le p,\quad 1\le t\le q . $$
The auxiliary variables $a_t$ encode the binary address of the selected variable. If $y_j$ is true, all the clauses belonging to $j$ force
$$ a_t=(-1)^{b_t} $$
for every bit $b_t$ of the binary representation of $2p-j$. Two different variables $y_i$ and $y_j$ cannot both be true, because their binary addresses differ in at least one bit, and the corresponding clauses would force opposite values for the same auxiliary variable. Thus the clauses enforce the at-most-one condition.
For the Langford problem, the original encoding contains many constraints of the form
$$ S_1(y_1,\ldots,y_p) $$
where $p$ is the number of possible locations of a particular pair or the number of pairs that could occupy a particular location. Whenever $p\ge7$, replace that instance of $S_1$ by the broadcast encoding above.
The effect of the replacement is determined by comparing the number of clauses. The binary encoding uses
$$ \sum_{j=1}^{p}\lfloor\lg(2p-j)\rfloor $$
clauses, because variable $y_j$ contributes one clause for each bit in the binary representation of $2p-j$. Since
$$ \lfloor\lg(2p-j)\rfloor\le \lfloor\lg(2p-1)\rfloor $$
for every $j$, the number of clauses is at most
$$ p\lfloor\lg(2p-1)\rfloor . $$
The auxiliary-variable count is
$$ \lfloor\lg p\rfloor . $$
The ordinary pairwise encoding of $S_1(y_1,\ldots,y_p)$ uses
$$ \binom p2=\frac{p(p-1)}2 $$
binary clauses and no auxiliary variables. For $p\ge7$ the new encoding has fewer clauses. For example, when $p=7$ the pairwise form has
$$ \binom72=21 $$
clauses, whereas the broadcast form has
$$ \begin{aligned} &\lfloor\lg 13\rfloor+\lfloor\lg 12\rfloor+\lfloor\lg 11\rfloor +\lfloor\lg 10\rfloor\ &\qquad+\lfloor\lg 9\rfloor+\lfloor\lg 8\rfloor+\lfloor\lg 7\rfloor\ &=3+3+3+3+3+3+2\ &=20 \end{aligned} $$
clauses and only
$$ \lfloor\lg7\rfloor=2 $$
auxiliary variables. The saving grows as $p$ increases because the old encoding grows quadratically while the new one grows as $O(p\lg p)$.
After replacing every occurrence with $p\ge7$, the resulting Langford formula has the same satisfying assignments on the original variables. The auxiliary variables only record the binary address of the chosen member of each at-most-one set. A satisfying assignment of the original variables extends to the auxiliary variables by assigning the address bits of the unique true $y_j$, and any satisfying assignment of the new formula restricts to a satisfying assignment of the original Langford formula because every replaced constraint is an equivalent encoding of $S_1$.
Hence the modified Langford encoding is equisatisfiable with the original one and uses the broadcast at-most-one construction for all large cardinality constraints.
$$ \boxed{\text{Replace every }S_1(y_1,\ldots,y_p)\text{ with }p\ge7\text{ by the }l=\lfloor\lg p\rfloor\text{-auxiliary-variable encoding above.}} $$