M. Benedetti, sKizzo: a QBF Decision Procedure based on Propositional Skolemization and Symbolic Reasoning, 2004.

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

M. Benedetti, sKizzo: A Suite to Evaluate and Certify QBFs, Proc. of 20th International Conference on Automated Deduction (CADE05), 2005.
DOI : 10.1007/11532231_27

M. Benedetti, The http://sKizzo.info web site, 2005.

R. E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, vol.35, issue.8, pp.35677-691, 1986.
DOI : 10.1109/TC.1986.1676819

H. K. Büning and X. Zhao, On Models for Quantified Boolean Formulas, Proc. of SAT'04, 2004.
DOI : 10.1007/978-3-540-25967-1_3

I. Gent and A. Rowley, Encoding Connect-4 using Quantified Boolean Formulae, 2003.

D. , L. Berre, M. Narizzano, L. Simon, and A. Tacchella, Second QBF solvers evaluation, avaliable on-line at www.qbflib.org, 2004.

J. Rintanen, Construction Conditional Plans by a Theoremprover, Journal of A. I. Research, pp.323-352, 1999.

J. Rintanen, Partial Implicit Unfolding in the Davis-Putnam Procedure for Quantified Boolean Formulae, Proceedings of the International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'01), 2001.
DOI : 10.1007/3-540-45653-8_25

L. J. Stockmeyer and A. R. Meyer, Word Problems Requiring Exponential Time, 5th Annual ACM Symposium on the Theory of Computing, 1973.

I. Wegener, Branching Programs and Binary Decision Diagrams, Monographs on Discrete Mathematics and Applications . SIAM, 2000.
DOI : 10.1137/1.9780898719789