TAOCP 7.2.2.2 Exercise 171
In Algorithm Y, `DFAIL` is the mechanism that records the failure of a descendant search so that the algorithm does not repeat the same unsuccessful computation after backtracking.
Section 7.2.2.2: Satisfiability
Exercise 171. [20] What is the purpose of DFAIL in Algorithm Y?
Verified: no
Solve time: 1m03s
Solution
In Algorithm Y, DFAIL is the mechanism that records the failure of a descendant search so that the algorithm does not repeat the same unsuccessful computation after backtracking.
Algorithm Y performs search with dependency-directed backtracking rather than chronological backtracking. When a branch fails, the contradiction is not merely evidence that the current assignment is impossible. The failure is analyzed to determine which earlier decisions were actually responsible for the contradiction. DFAIL stores this information in the form of a failure record associated with the responsible decision literals.
Suppose a later stage of the search reaches exactly the same relevant combination of decision literals. Without DFAIL, Algorithm Y would descend into the same subtree and rediscover the identical contradiction. With DFAIL, the stored failure is recognized immediately, the subtree is pruned, and control returns directly to the highest decision level involved in the recorded dependency.
Therefore DFAIL has two purposes. First, it prevents repeated exploration of search subtrees that have already been proved unsatisfiable. Second, it supplies the dependency information needed for non-chronological backtracking, allowing the algorithm to jump directly to the decision responsible for the failure instead of undoing irrelevant assignments one level at a time.
Hence DFAIL is the component that converts a failed search into reusable information, making the failure permanent until one of its responsible decision literals is changed. This is the essential mechanism by which Algorithm Y avoids redundant search. ∎