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: 2m11s

Let Algorithm B maintain a set $L$ of literals that is always strictly consistent, meaning it never contains both $x_i$ and $\neg x_i$ for any variable $x_i$, and it never contains duplicates. As in the original algorithm, the construction proceeds by a depth-first search over consistent extensions of $L$, where at each stage a new literal is chosen in accordance with the fixed ordering rules of Algorithm B (in particular, each extension corresponds to a choice for some previously unassigned variable or an admissible literal determined by the clause structure).

A set $L$ is called complete when for every variable $x_i$, exactly one of $x_i$ or $\neg x_i$ belongs to $L$. In this situation $L$ determines a total truth assignment $A_L$. A clause is said to be covered by $L$ if it contains at least one literal belonging to $L$ that makes it true under $A_L$. Thus, $L$ covers $F \cup T_n$ if and only if every clause is satisfied by the assignment induced by $L$.

Modification of Algorithm B

The original Algorithm B halts when it first reaches a complete consistent set $L$ that covers $F \cup T_n$. To enumerate all satisfying assignments, replace this halting step as follows:

When a complete consistent set $L$ is reached and $L$ covers $F \cup T_n$, output $L$, and then continue the search by backtracking to the most recent decision point where an untried consistent extension exists. The algorithm then resumes depth-first exploration from that state, excluding the already explored branch corresponding to $L$. The search terminates only when all backtracking possibilities are exhausted.

Correctness

1. Soundness of outputs

Let $L$ be any set output by the modified algorithm. By definition of the modification, $L$ is produced only when it is complete, strictly consistent, and covers $F \cup T_n$. Completeness and strict consistency imply that $L$ induces a well-defined truth assignment $A_L$.

If $L$ covers $F \cup T_n$, then every clause in the formula contains at least one literal that is true under $A_L$. Hence every clause is satisfied by $A_L$, so $A_L$ is a satisfying assignment.

Thus every output corresponds to a valid satisfying assignment.

2. Completeness

We show that every satisfying assignment is eventually output.

Let $A$ be any satisfying assignment. Construct the corresponding complete consistent literal set

$$ L_A = {x_i : A(x_i)=\text{true}} \cup {\neg x_i : A(x_i)=\text{false}}. $$

Consider the depth-first search tree implicitly generated by Algorithm B. Each node corresponds to a strictly consistent partial literal set, and each edge corresponds to a legal extension by one additional literal consistent with the current set.

We claim that Algorithm B explores every such node.

This follows from the defining structure of the algorithm: at each nonterminal node $L$, Algorithm B systematically selects a next admissible literal according to its fixed ordering rule and explores one extension completely before backtracking to explore the next alternative extension. Therefore, every consistent extension is eventually considered, because failure of one branch triggers backtracking to the nearest ancestor with an untried admissible choice, ensuring exhaustive traversal of all children at every node.

Since the search tree is finite (each variable can appear in at most one of two polarities, so depth is at most $n$), every branch is eventually either explored or pruned by inconsistency, and thus every leaf of the search tree is visited.

Because $L_A$ is a consistent complete assignment, it corresponds to a leaf of this search tree. Since all leaves are visited, $L_A$ is eventually reached and tested. As it satisfies all clauses, it is output.

Thus every satisfying assignment is produced.

3. Uniqueness (no duplicates)

Each node in the search tree corresponds to a strictly consistent set of literals constructed by a unique sequence of extension steps determined by the fixed ordering rule of Algorithm B. Because literals are never removed except by backtracking and are never reintroduced in a different order along the same path, no two distinct paths can produce the same consistent set $L$.

Formally, if two different root-to-node paths produced the same set $L$, then some literal would have to be introduced at two different decision levels or omitted and later reintroduced, contradicting strict consistency and the rule that each variable receives at most one assignment along any path.

Hence each complete assignment $L$ appears exactly once in the traversal, and therefore each satisfying assignment is output exactly once.

4. Termination

At each level of the search, a variable is assigned exactly one of two possible literals, and no variable is reconsidered along the same path. Hence the search tree has height at most $n$ and at most $2^n$ leaves. Each node is visited at most once due to depth-first backtracking with marking of exhausted alternatives.

Therefore the modified algorithm terminates after finitely many steps when all nodes of the finite search tree have been explored.

Conclusion

The modification replaces the single-solution halting condition with an output-and-backtrack step. The resulting depth-first traversal explores the entire finite search space of strictly consistent literal sets, outputs exactly those corresponding to satisfying assignments, and does so without repetition or omission. ∎