Extending DP to QBF

• Recent work in Artificial Intelligence

  • Cadoli, Giovanardi & Schaerf, AAAI 98, SAT 2000.
  • Rintanen, IJCAI 99

• Two main issues to deal with

  • correctness of quantifier dependencies

    • managing difference between
      "x.$ y. (x v y) & (-x v -y)
      $x. "y. (x v y) & (-x v -y)
    • set outermost quantified variable first, whatever type
  • different logic induced by universal quantification

    • algorithm breaks into cases depending on quantifier

Previous slide

Next slide

Back to first slide

View graphic version