{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T00:40:43Z","timestamp":1777596043839,"version":"3.51.4"},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2002,2,1]],"date-time":"2002-02-01T00:00:00Z","timestamp":1012521600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,2,1]],"date-time":"2002-02-01T00:00:00Z","timestamp":1012521600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[2002,2]]},"DOI":"10.1023\/a:1015019416843","type":"journal-article","created":{"date-parts":[[2002,12,28]],"date-time":"2002-12-28T22:07:59Z","timestamp":1041113279000},"page":"101-142","source":"Crossref","is-referenced-by-count":65,"title":["An Algorithm to Evaluate Quantified Boolean Formulae and Its Experimental Evaluation"],"prefix":"10.1007","volume":"28","author":[{"given":"Marco","family":"Cadoli","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Schaerf","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrea","family":"Giovanardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Massimo","family":"Giovanardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"395296_CR1","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1016\/0020-0190(79)90002-4","volume":"8","author":"B. Aspvall","year":"1979","unstructured":"Aspvall, B., Plass, M. F. and Tarjan, R. E.: A linear time algorithm for testing the truth of certain quantified Boolean formulas, Inform. Process. Lett.\n8 (1979), 121\u2013123.","journal-title":"Inform. Process. Lett."},{"key":"395296_CR2","first-page":"143","volume":"49","author":"M. Buro","year":"1993","unstructured":"Buro, M. and Kleine B\u00fcning, H.: Report on a SAT competition, EATCS Bull. 49 (1993), 143\u2013151.","journal-title":"EATCS Bull"},{"key":"395296_CR3","doi-asserted-by":"crossref","unstructured":"Cadoli, M., Giovanardi, A. and Schaerf, M.: Experimental analysis of the computational cost of evaluating quantified Boolean formulae, in Proceedings of the Fifth Conference of the Italian Association for Artificial Intelligence (AI*IA'97), Lecture Notes in Artif. Intell. 1321, Springer, 1997, pp. 207\u2013218.","DOI":"10.1007\/3-540-63576-9_109"},{"key":"395296_CR4","unstructured":"Cadoli, M., Giovanardi, A. and Schaerf, M.: An algorithm to evaluate quantified Boolean formulae, in Proceedings of the Fifteenth National Conference on Artificial Intelligence (AAAI'98), 1998, pp. 262\u2013267."},{"key":"395296_CR5","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1016\/0743-1066(93)90029-G","volume":"17","author":"M. Cadoli","year":"1993","unstructured":"Cadoli, M. and Schaerf, M.: A survey of complexity results for non-monotonic logics, J. Logic Programming\n17 (1993), 127\u2013160.","journal-title":"J. Logic Programming"},{"key":"395296_CR6","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1016\/0004-3702(95)00046-1","volume":"81","author":"J. Crawford","year":"1996","unstructured":"Crawford, J. and Auton, L.: Experimental results on the crossover point in random 3-SAT, Artificial Intelligence\n81 (1996), 31\u201357.","journal-title":"Artificial Intelligence"},{"key":"395296_CR7","unstructured":"Crawford, J. M. and Auton, L. D.: Experimental results on the crossover point in satisfiability problems, in Proceedings of the Eleventh National Conference on Artificial Intelligence (AAAI'93), 1993, pp. 21\u201327."},{"key":"395296_CR8","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/0004-3702(92)90018-S","volume":"57","author":"T. Eiter","year":"1992","unstructured":"Eiter, T. and Gottlob, G.: On the complexity of propositional knowledge base revision, updates and counterfactuals, Artificial Intelligence\n57 (1992), 227\u2013270.","journal-title":"Artificial Intelligence"},{"issue":"1","key":"395296_CR9","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1145\/200836.200838","volume":"42","author":"T. Eiter","year":"1995","unstructured":"Eiter, T. and Gottlob, G.: The complexity of logic-based abduction, J. ACM\n42(1) (1995), 3\u201342.","journal-title":"J. ACM"},{"key":"395296_CR10","unstructured":"Gent, I. P. and Walsh, T.: Beyond NP: The QSAT phase transition, in Proceedings of the Sixteenth National Conference on Artificial Intelligence (AAAI'99), 1999. Also available as APES report, APES-05-1998 from http:\/\/apes.cs.strath.ac.uk\/reports\/apes-05-1998.ps. gz."},{"key":"395296_CR11","unstructured":"Giunchiglia, E., Giunchiglia, F., Sebastiani, R. and Tacchella, A.: More evaluation of decision procedures formodal logics, in Proceedings of the Sixth International Conference on Principles of Knowledge Representation and Reasoning (KR'98), 1998, pp. 626\u2013635."},{"key":"395296_CR12","doi-asserted-by":"crossref","unstructured":"Giunchiglia, F. and Sebastiani, R.: Building decision procedures for modal logics from propositional decision procedures \u2014 the case study of modal K, in Proceedings of the Thirteenth International Conference on Automated Deduction (CADE'96), 1996a, pp. 583\u2013597.","DOI":"10.1007\/3-540-61511-3_115"},{"key":"395296_CR13","unstructured":"Giunchiglia, F. and Sebastiani, R.: A SAT-based decision procedure for ALC, in Proceedings of the Fifth International Conference on the Principles of Knowledge Representation and Reasoning (KR'96), 1996b, pp. 304\u2013314."},{"issue":"2","key":"395296_CR14","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1016\/0004-3702(95)00018-A","volume":"75","author":"J. Y. Halpern","year":"1995","unstructured":"Halpern, J. Y.: The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic, Artificial Intelligence\n75(2) (1995), 361\u2013372.","journal-title":"Artificial Intelligence"},{"key":"395296_CR15","unstructured":"Horrocks, I.: Using an expressive description logic: FaCT or fiction?, in Proceedings of the Sixth International Conference on Principles of Knowledge Representation and Reasoning (KR'98), 1998, pp. 636\u2013647."},{"key":"395296_CR16","doi-asserted-by":"crossref","unstructured":"Horrocks, I. and Patel-Schneider, P. F.: Optimising propositional modal satisfiability for description logic subsumption, in Proceedings of AISC-98, 1998.","DOI":"10.1007\/BFb0055916"},{"key":"395296_CR17","unstructured":"Hustadt, U. and Schmidt, R. A.: On evaluating decision procedures for modal logic, in Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence (IJCAI'97), 1997, pp. 202\u2013207."},{"key":"395296_CR18","unstructured":"Kautz, H. A. and Selman, B.: Pushing the envelope: Planning, propositional logic, and stochastic search, in Proceedings of the Thirteenth National Conference on Artificial Intelligence (AAAI'96), 1996, pp. 1194\u20131201."},{"key":"395296_CR19","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"H. Kleine B\u00fcning","year":"1995","unstructured":"Kleine B\u00fcning, H., Karpinski, M. and Fl\u00f6gel, A.: Resolution for quantified Boolean formulas, Inform. and Comput. 117 (1995), 12\u201318.","journal-title":"Inform. and Comput"},{"key":"395296_CR20","unstructured":"Rintanen, J.: Improvements to the evaluation of quantified Boolean formulae, in Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence (IJCAI'99), 1999, pp. 1192\u20131197."},{"key":"395296_CR21","unstructured":"Selman, B., Levesque, H. and Mitchell, D.: A new method for solving hard satisfiability problems, in Proceedings of the Tenth National Conference on Artificial Intelligence (AAAI'92), 1992, pp. 440\u2013446."},{"key":"395296_CR22","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1016\/0004-3702(95)00045-3","volume":"81","author":"B. Selman","year":"1996","unstructured":"Selman, B., Mitchell, D. and Levesque, H.: Generating hard satisfiability problems, Artificial Intelligence\n81 (1996), 17\u201329.","journal-title":"Artificial Intelligence"},{"key":"395296_CR23","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(76)90061-X","volume":"3","author":"L. J. Stockmeyer","year":"1976","unstructured":"Stockmeyer, L. J.: The polynomial-time hierarchy, Theoret. Comput. Sci.\n3 (1976), 1\u201322.","journal-title":"Theoret. Comput. Sci."},{"key":"395296_CR24","doi-asserted-by":"crossref","unstructured":"Stockmeyer, L. J. and Meyer, A. R.: Word problems requiring exponential time, in Proceedings of the Fifth ACM Symposium on Theory of Computing (STOC'73), 1973, pp. 1\u20139.","DOI":"10.1145\/800125.804029"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1015019416843.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1015019416843\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1015019416843.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:36:20Z","timestamp":1749123380000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1015019416843"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,2]]},"references-count":24,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2002,2]]}},"alternative-id":["395296"],"URL":"https:\/\/doi.org\/10.1023\/a:1015019416843","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2002,2]]}}}