Look-ahead

Look-ahead is a family of search heuristics in constraint satisfaction and satisfiability solving that evaluates the consequences of a candidate assignment before committing to it. Unlike forward checking, which only checks whether an assignment eliminates values from neighboring domains, look-ahead performs a deeper analysis — often a limited local search or propagation — to estimate how much the assignment would constrain the remaining problem.

The simplest look-ahead heuristic is forward degree: after a tentative assignment, count how many unassigned variables still have non-empty domains. A lower count means the assignment has propagated more constraints, which is generally desirable. More sophisticated heuristics compute the product of domain sizes or the entropy of the remaining search space. The unifying principle is that the solver should prefer assignments that maximize constraint propagation and minimize the expected size of the remaining search tree.

Look-ahead is computationally expensive. Each candidate assignment requires a local propagation step, and the number of candidate assignments at each search node is the product of the current domain sizes. In practice, solvers use restricted look-ahead: they only evaluate the most promising candidates or use cheaper approximations. The trade-off is characteristic of heuristic search: invest computational effort in evaluating moves to avoid investing effort in bad branches.

Look-ahead also serves a secondary function: nogood detection. If look-ahead reveals that no assignment to a particular variable can lead to a solution, the solver can record this as a nogood — a constraint that prevents the solver from repeating the same mistake. Nogood learning transforms a look-ahead failure into a permanent constraint, progressively tightening the problem as search proceeds. Modern SAT solvers like Chaff and MiniSat are essentially look-ahead engines with sophisticated nogood learning and conflict analysis.