An unusual preprocessing step

• Given a QSAT formula F

• Form existential simplification E(F)

  • Discard universal literals in F

• Solve E(F) as SAT problem (not as QSAT)

  • Use classic Davis-Putnam

• If DP succeeds, F is soluble as QSAT

  • Same values of e-variables works for all values of u-variables

Previous slide

Next slide

Back to first slide

View graphic version