質問

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.

正しい解決策はありません

ライセンス: CC-BY-SA帰属
所属していません cs.stackexchange
scroll top