New Algorithms for QBF
Outline
Quantified Boolean Formulae (QBF)
Complexity of QSAT
Applications of QBF
Davis Putnam Algorithm for SAT
Thrashing in Davis Putnam
Conflict Directed Backjumping
Formal proof of correctness Ö
Whatís coming up...
Extending DP to QBF
Solution Based Backjumping
St Andrews Algorithm
The Future
Email: ipg@dcs.st-and.ac.uk
Home Page: http://www.dcs.st-and.ac.uk/~ipg
Download presentation source