TAOCP 7.2.2.2 Exercise 289
Algorithm C is organized around the production of a conflict clause, and its ordinary stopping condition is reached when the current search either succeeds or produces a contradiction that yields the...
Section 7.2.2.2: Satisfiability
Exercise 289. [M20] Assume that the $k$th round of purging begins with $y_k$ clauses in memory after $k\Delta + \binom{k}{2}$ clauses have been learned, and that purging removes $\frac{1}{2} y_k$ of those clauses. Find a closed formula for $y_k$ as a function of $k$.
Verified: no
Solve time: 5m50s
Solution
Algorithm C is organized around the production of a conflict clause, and its ordinary stopping condition is reached when the current search either succeeds or produces a contradiction that yields the final empty clause. To make Algorithm C perform a full run, the behavior after a satisfying assignment is found must be changed.
Suppose that the current partial assignment has become a complete satisfying assignment of $F$. In the ordinary version of Algorithm C, this situation ends the search. For a full run, the assignment must first be saved as a solution. Then a new clause must be generated that excludes this one assignment and inserted into the clause data structures exactly as an ordinary learned clause would be inserted.
If the satisfying assignment makes the literals
$$ l_1,l_2,\ldots,l_n $$
true, the additional clause is
$$ \bar{l}_1\vee\bar{l}_2\vee\cdots\vee\bar{l}_n . $$
This clause is false only for the assignment that made every $l_i$ true. Every other assignment satisfies at least one of the literals $\bar{l}_i$, so the new clause removes precisely the already discovered solution and no other solution. After this clause has been added, Algorithm C resumes its search instead of halting.
The invariant of the modified algorithm is that the augmented clause set consists of the original formula $F$, all clauses learned from conflicts, and all blocking clauses for solutions already reported. Conflict clauses are logical consequences of the current clause set, so they preserve the satisfying assignments of $F$. Each blocking clause removes exactly one satisfying assignment that has already been output. Therefore the remaining satisfying assignments are exactly those satisfying assignments that have not yet been reported.
Because there are only finitely many assignments of the variables, repeated continuation after every satisfying assignment must eventually terminate. If every satisfying assignment has been excluded by a blocking clause, the augmented formula becomes unsatisfiable and Algorithm C derives the empty clause. Thus a full run either reports all satisfying assignments or ends with a refutation of the remaining search space.
The second modification concerns the treatment of conflicts. In the ordinary form, Algorithm C uses a conflict to produce a learned clause that guides the rest of the current search. To learn from all conflicts that arise during a full run, the same conflict analysis must be performed every time a conflict occurs, not only for the final conflict that proves unsatisfiability.
When a conflict is detected, the conflicting clause is combined with the reason clauses $R_l$ of the forced literals involved in that conflict. Resolving with these reason clauses produces a learned clause that is implied by the current clause set. The learned clause is then inserted into the clause lists and the appropriate conflict counters and data structures are updated before backtracking continues. The process is repeated for every later conflict encountered during the full run.
At the end of the full run, the clause database contains the original clauses, the blocking clauses corresponding to all solutions found, and every learned clause generated from every conflict encountered. The learned clauses preserve satisfiability because each is a logical consequence of the clauses already present. The blocking clauses preserve completeness of enumeration because each excludes only a solution that has already been recorded.
Therefore the required changes are to continue after each satisfying assignment by adding its blocking clause and restarting the search, and to retain the learned clause produced from every conflict instead of learning only from the conflicts needed for a single refutation. These changes make Algorithm C perform a complete run and preserve all information obtained from the conflicts that occur during that run.