TAOCP 7.2.2.2 Exercise 125

Exercise 125. ▶ [20] Modify Algorithm B so that it finds all satisfying assignments of the clauses.

Verified: yes
Solve time: 1m40s

Solution

Algorithm B already enumerates the complete binary search tree implicitly. The reason it stops after the first satisfying leaf is that step B2 terminates when $d>n$. To find all satisfying assignments, the successful leaf must be reported and the search must continue by backtracking instead of terminating.

Introduce the output operation $\operatorname{print}(m_1,\ldots,m_n)$, where the current values of the move array specify the chosen literals. The required modification is only at the success point of step B2.

Replace step B2 by the following.

$$ \textbf{B2. [Rejoice or choose.]} $$

If $d>n$, set

$$ \operatorname{print}(m_1,\ldots,m_n), $$

set $d\leftarrow n$, and go to B5. Otherwise set

$$ m_d\leftarrow [W_{2d}=0\ \text{or}\ W_{2d+1}\ne0] $$

and

$$ l\leftarrow 2d+m_d, $$

then continue with B3.

The remaining steps B1, B3, B4, B5, and B6 are unchanged.

The invariant of Algorithm B is that at the beginning of B2 the literals corresponding to $m_1,\ldots,m_{d-1}$ form a consistent partial assignment, and the watch structure represents the clauses after the assignments at levels $1,\ldots,d-1$ have been made. Steps B3 through B6 preserve this invariant while performing ordinary depth-first backtracking. A value of $d>n$ means that every variable has been assigned, so the current path satisfies every clause. Therefore the inserted $\operatorname{print}$ operation reports exactly the satisfying assignments reached by the search.

After printing, the assignment is not changed before step B5 is entered. Step B5 first tries the unused value of the current variable when such a value remains, and step B6 removes the current variable from the assignment stack when both values have been tried. Hence the algorithm eventually leaves the current leaf in the same way as the original Algorithm B leaves its successful leaf after termination.

Every satisfying assignment corresponds to exactly one path from $d=1$ to $d=n+1$, because each variable $x_d$ is assigned one of the two possible values encoded by $m_d$. The modified algorithm reaches that path because B5 and B6 exhaust both choices at every level. Conversely, a printed path satisfies all clauses because printing occurs only after B2 has reached $d>n$, which is reachable only after every call of B3 has succeeded. Thus no satisfying assignment is omitted and no nonsatisfying assignment is printed.

This completes the proof. ∎