TAOCP 7.2.2.2 Exercise 171

Section 7.2.2.2: Satisfiability

Exercise 171. [20] What is the purpose of DFAIL in Algorithm Y?

Verified: no
Solve time: 8m46s

Corrected solution:

Edit

DFAIL in Algorithm Y is a bookkeeping mechanism that records when a double-lookahead attempt has already been performed for a literal and has failed to produce useful information.

In Algorithm Y, the value DFAIL(l) is associated with each literal (l). It is initialized to zero. During a search state, when Algorithm Y performs double lookahead on a literal (l_0), the algorithm checks DFAIL(l_0) in step Y1. If

[ DFAIL(l_0)=ISTAMP, ]

the algorithm terminates the double-lookahead attempt immediately because the same literal has already been examined during the current search state.

If the double-lookahead procedure is carried out and does not find a contradiction or produce any useful implication, step Y6 sets

[ DFAIL(l_0)\leftarrow ISTAMP . ]

This records that the double-lookahead investigation for (l_0) has failed at the current timestamp.

The purpose of DFAIL is therefore to prevent repeated unsuccessful double-lookahead computations. Since double lookahead is an expensive operation, Algorithm Y avoids wasting time by remembering which literals have already been tested and found unproductive in the current context. It is a failure marker that allows the algorithm to skip redundant work while preserving the correctness of the search.