TAOCP 7.2.2.2 Exercise 122

Exercise 122. ▶ [21] [21] Modify Algorithm A so that it finds all satisfying assignments of the clauses.

Verified: no
Solve time: 2m23s

Solution

The original Algorithm A is designed to find one satisfying assignment. Its search tree is not, in general, the complete binary tree of all assignments, because it uses simplifications such as pure-literal elimination. Those simplifications are sufficient for finding one solution, but they are not sufficient for enumerating all solutions. Therefore the modification must remove every pruning operation that can discard satisfying assignments.

The first modification is the usual enumeration change. Whenever step A2 finds that the active clause set is empty, the algorithm must output the current assignment and then continue with step A6 rather than terminate. However, this is not enough, because Algorithm A may never visit some satisfying assignments.

In particular, the pure-literal steps must be modified. If a variable $x$ occurs only positively, Algorithm A may set $x=1$ immediately and omit the branch $x=0$. This is valid when only one satisfying assignment is required, because changing $x$ from $0$ to $1$ cannot destroy satisfiability. It is not valid when all satisfying assignments are required. For example,

$$ F=(x\lor y) $$

has the satisfying assignment

$$ (x,y)=(0,1), $$

although $x$ is a pure positive literal. Thus the branch $x=0$ must not be discarded.

The required modification is therefore as follows. Whenever Algorithm A would use a pure-literal assignment, replace that step by an ordinary branching step on that variable. Both possible values of the variable must be explored. All other simplifications that preserve the set of assignments represented by the search tree may remain unchanged, but any operation that deletes a possible value of a variable must be removed.

After these changes, the algorithm searches the complete assignment tree. The only modification to the stopping condition is that a satisfying leaf causes an output followed by backtracking.

To prove correctness, first consider any assignment output by the modified algorithm. Such an output occurs only when the active clause set is empty. During the search, each chosen branch fixes the value of one variable, and a clause is removed only when it has been satisfied by one of the chosen literals. Therefore, when no active clauses remain, every original clause contains a literal made true by the current assignment. Hence the output assignment satisfies $F$.

Conversely, let $A$ be any satisfying assignment of $F$. Because the modified algorithm branches on every variable instead of discarding branches through pure-literal elimination, the search tree contains the path obtained by choosing, at every branching variable, the value prescribed by $A$. None of the partial assignments on this path can produce a contradiction, because every partial assignment agrees with a satisfying complete assignment. Therefore the traversal eventually reaches the leaf corresponding to $A$. At that point every clause has already been satisfied, so step A2 outputs $A$.

It remains to account for variables that are not assigned on the current search path. In the modified algorithm every variable occurring in the formula must eventually be assigned by the branching process. If variables that do not occur in any clause are included in the definition of an assignment, they are independent of the formula and must be expanded separately: after a satisfying assignment to the occurring variables is found, all $2^k$ extensions over the $k$ absent variables must be output. If only variables occurring in $F$ are considered, no such expansion is necessary.

There are no duplicate outputs. Two different leaves of the complete branching tree differ at the first variable where their chosen values differ, and therefore represent different assignments. Since every variable choice is retained, every satisfying assignment corresponds to exactly one leaf.

Finally, after every satisfying leaf is output, step A6 performs the same backtracking operation that would have been performed after an unsuccessful branch. Hence the traversal continues until the entire search tree has been exhausted.

Thus the corrected enumeration algorithm is obtained by replacing successful termination in step A2 by output followed by backtracking, and by disabling pure-literal pruning so that both values of every variable remain available. The resulting algorithm outputs exactly all satisfying assignments of $F$. $\square$