Cadoli, M., Giovanardi, A., & Schaerf, M. (1998). An algorithm to evaluate quantified Boolean formulae. In *Proceedings of the 15th National Conference on Artificial Intelligence (AAAI98)*, pp. 262–267, Menlo Park, CA. AAAI Press.

Friedgut, E. (1998). Sharp thresholds of graph properties, and the k-sat problem. Journal of the American Mathematical Society, 12(4), 1017–1054.

Garey, M. R., & Johnson, D. S. (1979). *Computers and Intractability: A Guide to the Theory of* NP-Completeness. W. H. Freeman, New York.

Gent, I. P., MacIntyre, E., Prosser, P., Smith, B. M., & Walsh, T. (2001). Random constraint satisfaction: Flaws and structure. *Journal of Constraints*, 6(4), 345–372.

Gent, I. P., & Walsh, T. (1999). Beyond NP: The QSAT phase transition. In Proceedings of the Sixteenth National Conference on Artificial Intelligence and the Eleventh Innovative Applications of Artificial Intelligence Conference (AAAI-99), pp. 648–653, Menlo Park, CA. AAAI
Press.

Giunchiglia, E., Giunchiglia, F., Sebastiani, R., & Tacchella, A. (2000). SAT vs. Translation based decision procedures for modal logics: a comparative evaluation. *Journal of Applied NonClassical Logics,* 10(2), 145–172.

Giunchiglia, E., Giunchiglia, F., & Tacchella, A. (2002). SAT based decision procedures for classical modal logics. *Journal of Automated Reasoning*, 28, 143–171.

Giunchiglia, F., & Sebastiani, R. (1996). Building decision procedures for modal logics from propositional decision procedures - the case study of modal K. In Proceedings of the Thirteenth Conference on Automated Deduction, Vol. 1104 of *Lecture Notes in Artificial Intelligence*, pp. 583–597, Berlin. Springer.

Giunchiglia, F., & Sebastiani, R. (2000). Building decision procedures for modal logics from propositional decision procedures - the case study of modal K(m). Information and Computation, 162(1/2), 158–178.

Haarslev, V., & M¨oller, R. (2001). RACER system description. In *Proceedings of the International Joint Conference on Automated Reasoning, IJCAR'2001*, Vol. 2083 of Lecture Notes in Computer Science, pp. 701–705, Siena, Italy. Springer.

Halpern, J. Y. (1995). The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic. *Artificial Intelligence,* 75(3), 361–372.

Halpern, J. Y., & Moses, Y. (1992). A guide to the completeness and complexity for modal logics of knowledge and belief. *Artificial Intelligence,* 54(3), 319–379.

Heguiabehere, J., & de Rijke, M. (2001). The random modal QBF test set. In IJCAR'2001 Workshop on Issues in the Design and Experimental Evaluation of System for Modal and Temporal Logics, pp. 58–67.

Heuerding, A., J¨ager, G., Schwendimann, S., & Seyfreid, M. (1995). Propositional logics on the computer. In Baumgartner, P., H¨ahnle, R., & Posegga, J. (Eds.), *Automated Reasoning with* Analytic Tableaux and Related Methods: International Conference Tableaux'95, Vol. 918 of Lecture Notes in Artificial Intelligence, pp. 310–323, Berlin. Springer.

Heuerding, A., & Schwendimann, S. (1996). A benchmark method for the propositional modal logics K, KT, S4.. Tech. rep. IAM-96-015, University of Bern, Switzerland.