TAOCP 7.2.2.2 Exercise 27
Let $B_i$ denote the set of leaves below node $i$ in the binary tree used by Bailleux and Boufkhad's construction.
Section 7.2.2.2: Satisfiability
Exercise 27. [20] [20] Similarly, prove the correctness of Bailleux and Boufkhad's (20) and (21). Hint: They imply $b_j^i = 1$ whenever the leaves below node $k$ contain $j$ or more 1s.
Verified: no
Solve time: 3m27s
Solution
Let $B_i$ denote the set of leaves below node $i$ in the binary tree used by Bailleux and Boufkhad's construction. The intended meaning of the auxiliary variable $b_j^i$ is
$$ b_j^i=1 \iff \text{the leaves in }B_i\text{ contain at least }j\text{ variables assigned }1 . $$
We prove that clauses (20) and (21) enforce this implication in the direction required by the encoding: whenever the leaves below node $i$ contain $j$ or more $1$'s, the clauses force $b_j^i=1$.
For a leaf node $i$, the only possible nonzero count in its subtree is $1$. The clauses in (20) give the implication
$$ x_i=1 \implies b_1^i=1 . $$
Therefore the statement holds for every leaf: if the subtree contains at least one $1$, then $b_1^i$ is forced to $1$, and if it contains no $1$'s there is no requirement to force any $b_j^i$.
Now consider an internal node $i$ with children $i'$ and $i''$. Suppose that the leaves below $i$ contain at least $j$ $1$'s. Let the number of $1$'s in the left subtree be $k$ and the number in the right subtree be $j-k$ for some $k$ satisfying
$$ 0\le k\le j . $$
The induction hypothesis gives
$$ b_k^{i'}=1 $$
whenever the left subtree contains at least $k$ $1$'s, and
$$ b_{j-k}^{i''}=1 $$
whenever the right subtree contains at least $j-k$ $1$'s.
The clauses in (21) have the form
$$ (\bar b_k^{i'}\vee \bar b_{j-k}^{i''}\vee b_j^i), $$
for every allowable pair of indices. For the particular value of $k$ determined by the split of the $j$ ones between the two children, both antecedent literals are false:
$$ \bar b_k^{i'}=0,\qquad \bar b_{j-k}^{i''}=0 . $$
The clause therefore reduces to
$$ b_j^i=1 . $$
Hence every assignment containing at least $j$ true leaves below node $i$ forces the auxiliary variable $b_j^i$ to be true.
Applying this argument recursively from the leaves to the root proves that the variable corresponding to the root node is forced exactly when the complete set of leaves contains at least the forbidden number of $1$'s. The cardinality constraint encoded by (20) and (21) is therefore satisfied precisely when the clauses prevent the root variables representing excessive counts from becoming true.
This completes the proof. ∎