2
$\begingroup$

I am reading "Formalization and Implementation of Modern SAT Solvers", by Filip Marić.

My question is about how backjumping is defined. In an example [1], there is a conflict clause C equal to

[-1,-2,-3]

that has already been explained and learned. The decision trail is

|6, 1, 2, |7, |3, 4, 5,

where true decisions are marked with | and the others are propagated literals.

Then the algorithm performs a backjump to the level of literal 2, the most recently asserted literal that makes the conflict clause a unit clause. This modifies the decision trail to

|6, 1, 2

and immediately propagates -3 since [-1,-2,-3] is unit now, obtaining

|6, 1, 2, -3

What I would like to understand is: why not define backjumping so that the choice of 7, and all the (potential) work performed after it, were preserved? In this example, choosing 7 didn't do much, but it could have done a lot of propagation that we would not want to waste. There could also be other choices between 7 and -3 that we would benefit from preserving. It seems to me that the algorithm would be perfectly correct if it has backjumped to a decision trail

|6, 1, 2, |7, (any other choices not involved in the conflict, and literals propagated from 7 and them)

and then propagated -3 and got

|6, 1, 2, |7, (any other choices not involved in the conflict, and literals propagated from 7 and them), -3.

More generally, I am proposing that backjumping be defined not to go back to the most recent literal in C making it a unit clause (that is, 2), but to the most recent literal in the trail immediately before the last literal (-3) in C. That would be whatever is immediately before -3 in the trail, before the backjump, including 7, its propagations, and whatever other non-conflicting choices that happen to have been made.

Am I correct that this would be a better alternative that preserves work, or am I missing something?

[1] Fig. 6, trace of Example 7 if you are curious, but there is no need to go look as I think all the relevant information is here.

$\endgroup$
2
$\begingroup$

The intervening assignments between the current assignment and the backjump point might have been arrived at via considerable backtracking and backjumping themselves and it would be wasteful to repeat all that work. But in the context of a modern solver that work may not need to be repeated, because:

  • Any conflicts that occurred during the intervening assignments should have produced conflict clauses that rule out those time-wasting bad assignments in the immediate future.
  • Some solvers implement "phase saving" which remembers whether a variable was assigned true or false across backjumps (and restarts). So when DPLL chooses that variable again as a decision variable it will use the same true/false value, essentially picking up where it left off before the backjump.
  • The intervening assignments may not be repeated in the same order after the backjump. Solvers have heuristics that decide which variable becomes the next decision variable. These heuristics usually give preference to variables recently involved in conflicts, which usually has the effect of shuffling the decision variable order after every conflict.

There is another reason to backjump past 7 and then assert -3 and that is because of the way two-watched-literals works. Two-watched-literals is a clever algorithm for noticing when clauses are made unit by an assignment. It uses a lazy data structure that does not need to be updated for every clause referenced by an assignment and more importantly does not need to be updated at all when backtracking or backjumping. You can assume every SAT solver that implements DPLL also uses this algorithm to track unit clauses.

But in order for the lazy data structure to work there are procedural rules that must be followed. One of them is that you must roll back decision variable assignments and their unit propagations as a group. So to use your example, if -3 were asserted after the 7 assignment instead of before it and the 7 assignment were ever rolled back, then the -3 assignment would be undone separate from the |6 1 2 assignments that caused it. This would leave clause C, [-1 -2 -3], as a unit clause but two-watched-literals would not detect it. DPLL search is now broken and the solver may be confused enough to later claim that it has a satisfying assignment when it doesn't. If -3 is asserted together with the other consequences of the 6 assignment, then all the implications of that assignment will be rolled back together as they must be.

$\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.