Quantified satisfiability (QSAT)

• Existential quantifiers

  • as in propositional SAT

• Universal quantifiers

  • "x.$ y. (x v y) & (-x v -y)
  • x=true, then y=false satisfies
  • x=false, then y=true satisfies

• also called quantified Boolean formulae (QBF)

QSAT can be seen as an alternating game between existentials which want to make formula true, and universals which want to make it false

Previous slide

Next slide

Back to first slide

View graphic version