TAOCP 7.2.2.2 Exercise 23
Let $x_j$ denote the original variables and let $s_j^k$ denote the auxiliary variables used in the encoding of the symmetric threshold constraint $S_{\le r}(x_1,\ldots,x_n)$.
Section 7.2.2.2: Satisfiability
Exercise 23. [20] [20] Compare the clauses (18) and (19) to (20) and (21) in the case $n = 7$, $r = 4$.
Verified: no
Solve time: 2m24s
Solution
Let $x_j$ denote the original variables and let $s_j^k$ denote the auxiliary variables used in the encoding of the symmetric threshold constraint $S_{\le r}(x_1,\ldots,x_n)$.
For $n=7$ and $r=4$, the encoding given by (18) and (19) uses the variables
$$ x_1,\ldots,x_7,\quad s_1^1,\ldots,s_3^4, $$
so there are
$$ 7+(7-4)(4)=19 $$
literal occurrences of variables in the notation of the encoding, with $2n-4=10$ auxiliary variables. The clauses obtained from (18) and (19) form a lattice-like structure. Counting the clauses by the construction in (18) and (19), there are
$$ 5n-12=5\cdot7-12=23 $$
clauses.
The clauses from (20) and (21) use the tree decomposition of the $n$ inputs. For $n=7$, the leaves split into subtrees whose sizes are
$$ 4,\ 3,\ 2,\ 2,\ 1,\ 1,\ 1. $$
The corresponding auxiliary variables describe partial sums in these subtrees. The resulting clauses include the clauses
$$ \bar{7}s_6^1,\qquad \bar{6}s_6^1,\qquad \bar{6}\bar{7}s_6^2, $$
for the first node, and similarly
$$ \bar{5}s_5^1,\qquad \bar{4}s_5^1,\qquad \bar{4}\bar{5}s_5^2, $$
for the second node. Continuing through the remaining nodes gives the complete tree encoding. It introduces one additional auxiliary variable compared with (18) and (19), so it uses
$$ (2n-4)+1=11 $$
auxiliary variables.
The clause count can be obtained from the node structure. There are $\lfloor n/2\rfloor=3$ nodes covering two leaves, one node covering three leaves because $n\bmod2=1$, and $\lceil n/2\rceil=4$ nodes covering at least two levels. Hence the numbers of clauses are
$$ 3\cdot3+1\cdot5+4\cdot7+2=25. $$
Therefore, when $n=7$ and $r=4$, the encoding from (18) and (19) has $23$ clauses and $10$ auxiliary variables, while the encoding from (20) and (21) has $25$ clauses and $11$ auxiliary variables. The tree-based construction is therefore larger in this particular case.
$$ \boxed{\text{For }(n,r)=(7,4),\ (18)\text{--}(19)\text{ gives }23\text{ clauses and }10\text{ auxiliary variables, while }(20)\text{--}(21)\text{ gives }25\text{ clauses and }11\text{ auxiliary variables.}} $$