Fix backjumper - Githubissues

jgraley / inferno-cpp2v

2 stars 0 forks source link

Fix backjumper #511

Closed jgraley closed 2 years ago

jgraley commented 2 years ago

It's attempting graph-based backjumping but forgetting to keep considering earlier dead-ends.

jgraley commented 2 years ago

Commit c9933b8 fixes obvious bug in which ConstraintSet all_unsatisfied; was declared in the class and then never cleared down even though it's populated by unioning: all_unsatisfied = UnionOf(all_unsatisfied, unsatisfied);. I believe it needs to be cleared where I now declare it (making it a local variable).

There was no way backjumping could work because all_unsatisfied would end up holding every constraint that had ever been unsatisfied.

jgraley commented 2 years ago

I think the back-tracker is making the "standard mistake" of trying to make a second back-jump immediately after the first and jumping over variables that could fix the first conflict. Options therefore involve:

simplified graph-based by having a single global mode flag: set after backjump; don't backjump if set; clear on success for any variable
full graph-based is more sophisticated, can't do it with a single global mode, it works relative to depth into search space. Implement precisely per Dechter

jgraley commented 2 years ago

I think, in addition to fixing the bugs listed above, I also had to prevent backtracking when a leaf variable runs out of values having achieved one or more matches.

Backtracking now works as a result of these fixes.