Extending DP to QBF

• . . .

• If outermost quantifier is existential

  • set variable to true and recurse

    • if result is success, succeed
    • if result is failure,

      • set the variable to false and recurse

• If outermost quantifier is universal

  • set variable to true and recurse

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

      • set the variable to false and recurse

Previous slide

Next slide

Back to first slide

View graphic version