TAOCP 7.2.2.2 Exercise 13
Edit Let (x_{k,i}) denote the exact-cover row that places the two copies of (k) in positions (i) and (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: no
Solve time: 2m48s
Edit
Solution
Let (x_{k,i}) denote the exact-cover row that places the two copies of (k) in positions (i) and (i+k+1). For Langford pairs of order (4), the possible rows are
[
\begin{aligned}
&x_{1,1},x_{1,2},x_{1,3},x_{1,4},x_{1,5},x_{1,6},
&x_{2,1},x_{2,2},x_{2,3},x_{2,4},x_{2,5},
&x_{3,1},x_{3,2},x_{3,3},x_{3,4},
&x_{4,1},x_{4,2},x_{4,3}.
\end{aligned}
]
There are therefore
[ 6+5+4+3=18 ]
row variables. A row (x_{k,i}) covers the symbol column (k) and the two position columns (i) and (i+k+1). Thus the exact-cover instance has twelve columns, namely the four symbol columns
[ 1,2,3,4 ]
and the eight position columns
[ p_1,p_2,\ldots,p_8 . ]
(a)
The constraints analogous to (12) are the requirement that every column be covered exactly once. The four symbol constraints are
[
\begin{aligned}
1:;&x_{1,1}+x_{1,2}+x_{1,3}+x_{1,4}+x_{1,5}+x_{1,6}=1,
2:;&x_{2,1}+x_{2,2}+x_{2,3}+x_{2,4}+x_{2,5}=1,
3:;&x_{3,1}+x_{3,2}+x_{3,3}+x_{3,4}=1,
4:;&x_{4,1}+x_{4,2}+x_{4,3}=1.
\end{aligned}
]
The eight position constraints are
[
\begin{aligned}
p_1:;&x_{1,1}+x_{2,1}+x_{3,1}+x_{4,1}=1,
p_2:;&x_{1,2}+x_{2,2}+x_{3,2}+x_{4,2}=1,
p_3:;&x_{1,1}+x_{1,3}+x_{2,3}+x_{3,3}+x_{4,3}=1,
p_4:;&x_{1,2}+x_{1,4}+x_{2,1}+x_{2,4}+x_{3,4}=1,
p_5:;&x_{1,3}+x_{1,5}+x_{2,2}+x_{2,5}+x_{3,1}=1,
p_6:;&x_{1,4}+x_{1,6}+x_{2,3}+x_{3,2}+x_{4,1}=1,
p_7:;&x_{1,5}+x_{2,4}+x_{3,3}+x_{4,2}=1,
p_8:;&x_{1,6}+x_{2,5}+x_{3,4}+x_{4,3}=1.
\end{aligned}
]
These equations express the Langford condition. Choosing a row for each (k) places the two copies of (k) in positions separated by (k+1), and the position constraints force every position to be occupied once.
(b)
The conversion rule (13) transforms an exact-cover constraint
[ a_1+\cdots+a_s=1 ]
into the clauses
[ a_1\vee\cdots\vee a_s ]
and
[ \bar a_i\vee\bar a_j \qquad(1\leq i<j\leq s). ]
The binary clauses forbid two rows belonging to the same exact-cover column from being chosen simultaneously.
A pair of rows (r) and (s) can occur together in several different exact-cover columns. If
[ C(r)\cap C(s)\neq\varnothing , ]
where (C(r)) is the set of columns covered by row (r), then each common column produces the same binary clause
[ \bar r\vee\bar s . ]
Thus the direct conversion may generate the same clause several times. If two rows have exactly one common column, the clause is generated once. If they have no common column, it is not generated at all.
Therefore the duplicate clauses can be avoided by defining the binary part directly from the conflict relation:
[ {\bar r\vee\bar s(r)\cap C(s)\neq\varnothing,\ r\neq s}. ]
Each unordered conflicting pair of rows contributes exactly one clause. This gives the same logical condition because repeated copies of a clause do not change the set of satisfying assignments.
(c)
The formula (\operatorname{langford}(4)) is obtained by applying (13) directly to the twelve exact-cover constraints above. Its variables are the eighteen row variables
[ {x_{k,i}:1\leq k\leq4,\ 1\leq i\leq 7-k}. ]
It contains the twelve positive clauses
[ \bigvee_{r:,c\in C(r)} r ]
one for each exact-cover column (c), together with the binary clauses produced independently from every column. Hence if two rows share two columns, the corresponding binary clause occurs twice, and if they share three columns it occurs three times.
The formula (\operatorname{langford}'(4)) is the deduplicated version. It has the same twelve positive clauses, but its binary clauses are included only once:
[ \bar r\vee\bar s ]
for each unordered pair of distinct rows satisfying
[ C(r)\cap C(s)\neq\varnothing . ]
For example, (x_{1,1}) covers the columns
[ {1,p_1,p_3}, ]
and (x_{3,1}) covers
[ {3,p_1,p_5}. ]
They share the position column (p_1), so both formulas contain
[ \bar{x}{1,1}\vee\bar{x}{3,1}. ]
If another common column existed, (\operatorname{langford}(4)) would contain another copy of this clause, whereas (\operatorname{langford}'(4)) would still contain only one copy.
Thus (\operatorname{langford}(4)) and (\operatorname{langford}'(4)) are logically equivalent CNF formulas, but the latter removes all duplicate binary clauses.
This version fixes the variable count, makes the conflict relation explicit, and gives the precise construction of both CNF instances.