9
$\begingroup$

On the wikipedia page here it describes pretty well the CDCL algorithm (and it seems the pictures were taken from slides created by Sharad Malik at Princeton). However when describing how to backtrack all it says is "to the appropriate point". MiniSAT also uses a variant of the CDCL algorithm so I read this paper. What they seem to say is that you should backtrack until the learned clause is a unit clause. That is certainly clarification but it doesn't make sense to me. The last assignment is definitely going to be part of the learned conflict clause as far as I can tell (perhaps I am wrong here?) so when you backtrack one step you will immediately make the learned clause unit, the last assigned value will flip, and the algorithm will proceed exactly as DPLL without ever backtracking sufficiently far. Additionally the wikipedia page doesn't follow this rule, it backtracks much further as seems desirable.

How far is one supposed to backtrack?

$\endgroup$
7
$\begingroup$

Here's the relevant paragraph from the MiniSAT paper:

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.