Quantified Boolean Formulae (QBF)

• 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

• Solution is a strategy

• also called quantified satisfiability (QSAT)

QBF 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