Chapter 3 "Complete Algorithms" of Handbook of Satisfiability is a good introduction to the modern SAT solver algorithms. Today I learned far-backtracking which is different from simple non-chronological backtracking.
In simple non-chronological backtracking scheme, conflict set is constructed from contradiction and implication graph, and then backtrack to the most recent decision variable in the conflict set.
In far-backtracking scheme, conflict driven clause is learned, and then backtrack to the second highest decision level in the clause. This level is the deepest level at which the learnt clause can cause unit propagation.
> +Takeo Imai Far backtracking is most common in modern SAT solvers. It is tightly integrated with conflict learning, and I think it's faster to fix the cause of conflict.
> +Eunsuk Kang I'm just interested in the internal of SAT solvers. But I might write a simple one to aid my understanding.
In far-backtracking scheme, conflict driven clause is learned, and then backtrack to the second highest decision level in the clause. This level is the deepest level at which the learnt clause can cause unit propagation.
Far backtracking is most common in modern SAT solvers.
It is tightly integrated with conflict learning, and I think it's faster to fix the cause of conflict.
> +Eunsuk Kang
I'm just interested in the internal of SAT solvers.
But I might write a simple one to aid my understanding.