SAT solving
Backtracking
Returning to an earlier search state after a conflict.
Definition
Backtracking
Backtracking removes provisional assignments that belong to a failed SAT search branch.
CDCL can backtrack to the highest decision level that still matters to the learned clause. The new clause then forces a different continuation or blocks the same conflict.
01
Example
If a decision at level two caused the conflict and level three was unrelated, the solver can return directly to level one.
02
Important distinction
Backtracking changes the current search state but does not remove the original clauses or invalidate a justified learned clause.
After reading this article, you should be able to
- Define Backtracking in the sense used on this site.
- Identify the assignments removed by chronological and non-chronological backtracking.