Backjumps

Backjumps, or backjumping, is a technique used in satisfiability solving and related search algorithms to perform non-chronological backtracking after encountering a conflict. Instead of simply undoing the most recent decision, the solver jumps directly to an earlier decision level that is determined to be relevant to the conflict.

In conflict-driven clause learning (CDCL) solvers, the search process records decisions and implications on a stack of decision levels. When a conflict arises, the solver analyzes the conflict to derive a learned clause and identify the most relevant decision level (often associated with the first unique implication point). The learned clause reveals which earlier decisions contributed to the conflict, allowing the solver to backtrack to the highest such level. The learned clause is then asserted, typically becoming unit under the backjumped assignment, and propagation resumes. This non-chronological backtracking prunes large portions of the search space that would have been explored with simple backtracking.

History and variants: Backjumping grew out of non-chronological backtracking in DPLL-based approaches and was strengthened by the introduction of conflict-driven clause learning in the 1990s. Modern SAT solvers rely on backjumps as a core mechanism for efficiency, with the exact backjump length determined by conflict analysis and the learned clause. Solvers may combine backjumps with restarts, clause database management, and decision-level heuristics to further optimize performance.

See also: DPLL, CDCL, clause learning, non-chronological backtracking.