C. Ansotegui, C. Gomes, and B. Selman, Achilles' heel of QBF, AAAI, 2005.

A. Ayari and D. Basin, Qubos: Deciding Quantified Boolean Logic Using Propositional Satisfiability Solvers, Formal Methods in Computer-Aided Design, Fourth International Conference, 2002.
DOI : 10.1007/3-540-36126-X_12
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.18.2608

A. Ayari, D. Basin, and S. Friedrich, Structural and behavioral modeling with monadic logics, Proceedings 1999 29th IEEE International Symposium on Multiple-Valued Logic (Cat. No.99CB36329), pp.142-151, 1999.
DOI : 10.1109/ISMVL.1999.779709
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.42.8710

M. Benedetti, Evaluating QBFs via Symbolic Skolemization, Proc. of the 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR04), number 3452, 2005.
DOI : 10.1007/978-3-540-32275-7_20
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.592.4153

M. Benedetti, Extracting Certificates from Quantified Boolean Formulas, Proc. of 9th International Joint Conference on Artificial Intelligence (IJCAI05), 2005.

A. Biere, Resolve and Expand, SAT, 2004.
DOI : 10.1007/11527695_5

L. Bordeaux, Boolean and interval propagation for quantified constraints, First International Workshop on Quantification in Constraint Programming, 2005.

M. Cadoli, M. Schaerf, A. Giovanardi, and M. Giovanardi, An algorithm to evaluate quantified boolean formulae and its experimental evaluation, Journal of Automated Reasoning, vol.28, issue.2, pp.101-142, 2002.
DOI : 10.1023/A:1015019416843

M. Davis, G. Logemann, and D. Loveland, A machine program for theorem-proving, Communication of the ACM, vol.5, 1962.

U. Egly, M. Seidl, and S. Woltran, A solver for QBFs in nonprenex form, ECAI, pp.477-481, 2006.

E. Giunchiglia, M. Narizzano, and A. Tacchella, QuBE: A System for Deciding Quantified Boolean Formulas Satisfiability, IJCAR, pp.364-369, 2001.
DOI : 10.1007/3-540-45744-5_27

E. Giunchiglia, M. Narizzano, and A. Tacchella, Backjumping for Quantified Boolean Logic satisfiability, Artificial Intelligence, vol.145, issue.1-2, pp.99-120, 2003.
DOI : 10.1016/S0004-3702(02)00373-9

R. Letz, Lemma and Model Caching in Decision Procedures for Quantified Boolean Formulas, TABLEAUX Vardi. Symbolic decision procedures for QBF International Conference on Principles and Practice of Constraint Programming, pp.160-175, 2002.
DOI : 10.1007/3-540-45616-3_12

D. A. Plaisted, A. Biere, and Y. Zhu, A satisfiability procedure for quantified Boolean formulae, Discrete Applied Mathematics, vol.130, issue.2, pp.291-328, 2003.
DOI : 10.1016/S0166-218X(02)00409-2

J. Rintanen, Improvements to the evaluation of quantified boolean formulae, IJCAI, pp.1192-1197, 1999.

J. Rintanen, Partial Implicit Unfolding in the Davis-Putnam Procedure for Quantified Boolean Formulae, Workshop on Theory and Applications of QBF, Int. Join Conference on Automated Reasoning, 2001.
DOI : 10.1007/3-540-45653-8_25

M. Sheeran and G. Stålmarck, A Tutorial on St??lmarck???s Proof Procedure for Propositional Logic, Formal Methods in Computer-Aided Design, pp.82-99, 1998.
DOI : 10.1007/3-540-49519-3_7
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.23.3693

I. Stéphan, Finding models for quantified boolean formulae, First International Workshop on Quantification in Constraint Programming, 2005.

I. Stéphan, Boolean propagation based on literals for quantified boolean formulae, 17th European Conference on Artificial Intelligence, 2006.

L. Zhang, Solving QBF with combined conjunctive and disjunctive normal form, National Conference on Artificial Intelligence, 2006.

L. Zhang and S. Malik, Conflict driven learning in a quantified Boolean Satisfiability solver, Proceedings of the 2002 IEEE/ACM international conference on Computer-aided design , ICCAD '02, 2002.
DOI : 10.1145/774572.774637