Conflict-Driven Search

Conflict-driven search is a computational paradigm in which the primary engine of progress is not success but failure. Rather than treating dead ends as mere obstacles to be avoided, conflict-driven systems — most prominently CDCL-based SAT solvers — analyze each contradiction to extract structural information that reshapes the remaining search space. Every conflict becomes a lesson; every dead end becomes a new constraint. The result is a search process that learns from its own mistakes in real time, transforming what appears to be blind trial-and-error into an emergent theory-building exercise.

The paradigm extends beyond boolean satisfiability. In automated theorem proving, conflict-driven techniques guide proof search by learning lemmas from failed proof attempts. In constraint programming, nogood learning performs an analogous function, recording combinations that cannot occur and propagating this knowledge across the search tree. In planning and scheduling, conflict analysis identifies resource bottlenecks that would not be visible from a purely forward-search perspective. The common thread is the recognition that search is not exploration of a static landscape but a dialogue with a problem that talks back — and that the most informative responses come from the places where the dialogue breaks down.

The efficiency gains of conflict-driven search are not incremental improvements. They are qualitative phase shifts. A search that merely backtracks chronologically forgets its failures; a search that learns from them remembers. Memory is the difference between exponential and tractable.