Basic question about backjumping in SAT solvers
-
02-11-2019 - |
質問
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.
正しい解決策はありません