Solution Based Backjumping

• Enrico Giunchiglia, Tacchella, Narizzano, IJCAI-01

• change universal backtracking part of QBF algorithm Ö

• If outermost quantifier is universal

  • set variable to true and recurse

    • if result is failure, fail
    • if result is success,

      • if current variable not involved in solution set, succeed
      • set the variable to false and recurse

• ìsolution setî = set of universal variables essential to successes in any part of failed search

• reduces thrashing on some benchmark problems

Previous slide

Next slide

Back to first slide

View graphic version