Asked By : Jake
Answered By : Kyle Jones
The decision phase will continue until either all variables have been assigned, in which case we have a model, or a conflict has occurred. On conflicts, the learning procedure will be invoked and a conflict clause producted. The trail will be used to undo decision, one level at a time, until precisely one of the literals of the learnt clause becomes unbound (they are all $False$ at the point of conflict). By construction, the conflict clause cannot go directly from conflict to a clause with two or more unbound literals. If the clause remains unit for several decision levels, it is advantageous to chose [sic] the lowest level (referred to as backjumping or non-chronological backtracking).
A point you seem to have missed is that once the learned clause becomes unit due to undone assignments (backtracking), the solver doesn’t stop there. There could be other assignments before this one that have no bearing on the current conflict and experimentally it has been shown that it is better to undo these unrelated assignments also. So the solver continues to undo assignments until the next undo would make the learned clause non-unit, i.e. it would contain more than one unassigned variable. The solver stops here, runs unit propagation to satisfy the unit clause and then resumes the search, assigning variables normally. Note also that the current decision variable may not be present in the learned clause. A common strategy for a CDCL solver is to find the first unique implication point and use that variable in the learned clause. In some cases the first UIP is the decision variable, but often it is not.
Best Answer from StackOverflow
Question Source : http://cs.stackexchange.com/questions/43027 Ask a Question Download Related Notes/Documents