TAOCP 7.2.2.2 Exercise 122

We restate Algorithm A in the only way relevant to the modification: it performs a depth-first backtracking search over partial consistent sets of literals $L$, with choice points where a literal is s...

taocpmathematicsalgorithmsvolume-4medium

Section 7.2.2.2: Satisfiability

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

Verified: yes
Solve time: 2m20s

We restate Algorithm A in the only way relevant to the modification: it performs a depth-first backtracking search over partial consistent sets of literals $L$, with choice points where a literal is selected, propagation steps (unit and forced assignments), a contradiction test, and a success test when every clause is satisfied.

Let $F$ be the set of clauses. Let $L$ be the current consistent set of literals maintained by the algorithm. The original Algorithm A has a terminal step:

  • A8 (original): if every clause $C \in F$ is satisfied by $L$, then halt and report success.

All other steps, in particular the branching choice step (A3), propagation and simplification steps (A4), and backtracking steps (A7), remain unchanged.

The modification consists solely in replacing the terminal behavior at A8 so that the search does not stop at the first solution, but continues exhaustively through the search tree.

Modified step A8 (replacement of termination)

A8 (modified): If every clause $C \in F$ is satisfied by $L$, then:

  1. Output the assignment induced by $L$.
  2. Mark the current search node as fully explored (so it will not be revisited).
  3. Force backtracking as in A7: locate the most recent decision level at which an untried alternative choice remains.
  • If such a level exists, undo all assignments above that level, and proceed with the next alternative branch exactly as prescribed by A7 and A3.
  • If no such level exists, terminate the algorithm.

Crucially, no new branching rule is introduced and no modification is made to propagation or consistency checking. The only change is that a successful leaf is no longer absorbing.

Why this correctly enumerates all satisfying assignments

The execution of Algorithm A defines a finite search tree:

  • Each node corresponds to a consistent partial assignment $L$.
  • Each edge corresponds to a single branching decision introduced at A3.
  • Propagation steps (A4 and forced consequences) are deterministic given the current branch.

Thus every complete path from the root to a leaf corresponds to a uniquely determined set of decisions, hence to a unique maximal consistent literal set.

A satisfying assignment is exactly a leaf where all clauses are satisfied. Therefore:

  • Every satisfying assignment appears as at least one successful leaf, since the algorithm explores all branches of the finite decision tree.
  • No satisfying assignment is produced twice, because the algorithm performs a depth-first traversal that never re-enters an already completed subtree. Once A8 triggers at a leaf, the backtracking step moves to the next unexplored alternative at the nearest choice point, and the entire subtree below the completed leaf is never revisited.

This establishes injectivity of outputs: each output arises from exactly one completed root-to-leaf traversal, and that traversal is not repeated.

Correctness of backtracking continuation

The backtracking mechanism is unchanged from Algorithm A. The modification does not introduce any looping behavior because:

  • Each execution of A8 at a leaf permanently marks that leaf as processed.
  • Backtracking always moves strictly upward in the finite decision tree to the nearest untried branch.
  • The number of branches is finite, since each variable/literal decision reduces a finite space of choices.

Hence every step either advances into a new unexplored branch or terminates when all branches are exhausted.

Termination

The underlying search space is a finite tree determined by the finite set of variables and branching choices in Algorithm A. Each edge of this tree is traversed at most once in a depth-first traversal. Since A8 no longer halts globally but only redirects control to backtracking, the only possible termination condition is exhaustion of all branches. Therefore the modified algorithm terminates exactly when the original search space is exhausted.

Conclusion

Replacing the halting action in step A8 by output plus controlled backtracking converts Algorithm A from a decision procedure into a complete enumeration procedure. The modified algorithm traverses the same finite search tree, outputs exactly those leaves that satisfy all clauses, and guarantees that every satisfying assignment is produced exactly once before termination.