{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:35:31Z","timestamp":1725561331842},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540208518"},{"type":"electronic","value":"9783540246053"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24605-3_35","type":"book-chapter","created":{"date-parts":[[2010,7,29]],"date-time":"2010-07-29T08:50:35Z","timestamp":1280393435000},"page":"468-485","source":"Crossref","is-referenced-by-count":15,"title":["Challenges in the QBF Arena: the SAT\u201903 Evaluation of QBF Solvers"],"prefix":"10.1007","author":[{"given":"Daniel","family":"Le Berre","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laurent","family":"Simon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Armando","family":"Tacchella","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"35_CR1","unstructured":"Scholl, C., Becker, B.: Checking equivalence for partial implementations. Technical report, Institute of Computer Science, Albert-Ludwigs University (October 2000)"},{"key":"35_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/10722167_11","volume-title":"Computer Aided Verification","author":"A. Ayari","year":"2000","unstructured":"Ayari, A., Basin, D.: Bounded model construction for monadic second-order logics. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 99\u2013113. Springer, Heidelberg (2000)"},{"key":"35_CR3","first-page":"1192","volume-title":"Proceedings of the Sixteenth International Joint Conferences on Artificial Intelligence (IJCAI 1999)","author":"J. Rintanen","year":"1999","unstructured":"Rintanen, J.: Improvements to the evaluation of quantified boolean formulae. In: Proceedings of the Sixteenth International Joint Conferences on Artificial Intelligence (IJCAI 1999), Stockholm, Sweden, July 31-August 6, pp. 1192\u20131197. Morgan Kaufmann, San Francisco (1999)"},{"issue":"1","key":"35_CR4","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/S0004-3702(02)00375-2","volume":"147","author":"C. Castellini","year":"2003","unstructured":"Castellini, C., Giunchiglia, E., Tacchella, A.: Sat-based planning in complex domains: Concurrency, constraints and nondeterminism. Artificial Intelligence\u00a0147(1), 85\u2013117 (2003)","journal-title":"Artificial Intelligence"},{"key":"35_CR5","doi-asserted-by":"crossref","unstructured":"Pan, G., Vardi, M.Y.: Optimizing a BDD-based modal solver. In: Proceedings of the Nineteenth Internations Conference on Automated Deduction (2003) (to appear)","DOI":"10.1007\/978-3-540-45085-6_7"},{"issue":"3","key":"35_CR6","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM\u00a07(3), 201\u2013215 (1960)","journal-title":"Journal of the ACM"},{"issue":"7","key":"35_CR7","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM\u00a05(7), 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"key":"35_CR8","unstructured":"Cadoli, M., Giovanardi, A., Schaerf, M.: An algorithm to evaluate quantified boolean formulae. In: Proceedings of the Fifteenth National Conference on Artificial Intelligence (AAAI 1998) Madison, Wisconsin, USA, pp. 262\u2013267 (1998)"},{"key":"35_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1007\/3-540-45653-8_25","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"J. Rintanen","year":"2001","unstructured":"Rintanen, J.: Partial implicit unfolding in the Davis-Putnam procedure for quantified Boolean formulae. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol.\u00a02250, pp. 362\u2013376. Springer, Heidelberg (2001)"},{"key":"35_CR10","unstructured":"Feldmann, R., Monien, B., Schamberger, S.: A distributed algorithm to evaluate quantified boolean formula. In: Proceedings of the Seventeenth National Conference in Artificial Intelligence (AAAI 2000), pp. 285\u2013290 (2000)"},{"key":"35_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-46135-3_14","volume-title":"Principles and Practice of Constraint Programming - CP 2002","author":"L. Zhang","year":"2002","unstructured":"Zhang, L., Malik, S.: Towards a symmetric treatment of satisfaction and conflicts in quantified boolean formula evaluation. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol.\u00a02470, pp. 200\u2013215. Springer, Heidelberg (2002)"},{"key":"35_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/3-540-45744-5_27","volume-title":"Automated Reasoning","author":"E. Giunchiglia","year":"2001","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: QuBE: A system for deciding Quantified Boolean Formulas Satisfiability. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 364\u2013369. Springer, Heidelberg (2001)"},{"key":"35_CR13","unstructured":"Letz, R.: Advances in decision procedures for quantified boolean formulas. In: Proceedings of the First International Workshop on Quantified Boolean Formulae (QBF 2001), pp. 55\u201364 (2001)"},{"key":"35_CR14","unstructured":"Rowley, A.G.D., Gent, I.P., Hoos, H.H., Smyth, K.: Using stochastic local search to solve quantified boolean formulae. Technical Report APES-58-2003, APES Research Group (January 2003)"},{"issue":"2","key":"35_CR15","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1023\/A:1015019416843","volume":"28","author":"M. Cadoli","year":"2002","unstructured":"Cadoli, M., Schaerf, M., Giovanardi, A., Giovanardi, M.: An algorithm to evaluate quantified boolean formulae and its experimental evaluation. Journal of Automated Reasoning\u00a028(2), 101\u2013142 (2002)","journal-title":"Journal of Automated Reasoning"},{"key":"35_CR16","unstructured":"Gent, I.P.: Beyond N.P: The QSAT phase transition. In: Proceedings of the Sixteenth National Conference on Artificial Intelligence (AAAI 1999), pp. 648\u2013 653 (1999)"},{"key":"35_CR17","first-page":"459","volume-title":"Proceedings of the Tenth National Conference on Artificial Intelligence","author":"D.G. Mitchell","year":"1992","unstructured":"Mitchell, D.G., Selman, B., Levesque, H.J.: Hard and easy distributions for SAT problems. In: Proceedings of the Tenth National Conference on Artificial Intelligence, pp. 459\u2013465. AAAI Press, Menlo Park (1992)"},{"key":"35_CR18","doi-asserted-by":"crossref","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: On the effectiveness of backjumping and trivial truth in quantified boolean formulas satisfiability. In: Proceedings of the First International Workshop on Quantified Boolean Formulas (QBF 2001), pp. 40\u201354 (2001)","DOI":"10.1007\/3-540-45411-X_13"},{"key":"35_CR19","unstructured":"Sixth International Conference on Theory and Applications of Satisfiability Testing, S. Margherita Ligure - Portofino ( Italy) (May 2003)"},{"key":"35_CR20","doi-asserted-by":"crossref","unstructured":"Simon, L., Chatalic, P.: SATEx: a web-based framework for SAT experimentation. In: Kautz, H., Selman, B. (eds.), June 2001. Electronic Notes in Discrete Mathematics, vol.\u00a09, Elsevier Science Publishers, Amsterdam (2001), http:\/\/www.lri.fr\/simon\/satex\/satex.php3","DOI":"10.1016\/S1571-0653(04)00318-X"},{"key":"35_CR21","unstructured":"Narizzano, M.: QBFLIB - The Quantified Boolean Formulas Satisfiability Library, http:\/\/www.qbflib.org"},{"key":"35_CR22","unstructured":"Audemard, G., Le Berre, D., Roussel, O., Lynce, I., Marques Silva, J.: OpenSAT: An Open Source SAT Software Project. In: Sixth International Conference on Theory and Applications of Satisfiability Testing [19]"},{"key":"35_CR23","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference, DAC 2001, June 2001, pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"35_CR24","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/BF02127976","volume":"17","author":"M. Bohm","year":"1996","unstructured":"Bohm, M., Speckenmeyer, E.: A fast parallel sat\u2013solver \u2014 efficient workload balancing. Annals of Mathematics and Artificial Intelligence\u00a017, 381\u2013400 (1996)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"35_CR25","first-page":"143","volume":"49","author":"M. Buro","year":"1993","unstructured":"Buro, M., Kleine B\u00fcning, H.: Report on a SAT competition. Bulletin of the European Association for Theoretical Computer Science\u00a049, 143\u2013151 (1993)","journal-title":"Bulletin of the European Association for Theoretical Computer Science"},{"key":"35_CR26","doi-asserted-by":"crossref","unstructured":"Zhang, L., Malik, S.: Conflict driven learning in a quantified boolean satisfiability solver. In: Proceedings of International Conference on Computer Aided Design (ICCAD 2002) San Jose, CA, USA (November 2002)","DOI":"10.1145\/774572.774637"},{"key":"35_CR27","unstructured":"Biere, A.: Personal communications (2003)"},{"key":"35_CR28","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: Backjumping for quantified boolean logic satisfiability. In: Proceedings of the Seventeenth International Joint Conferences on Artificial Intelligence (IJCAI 2001), Seattle, Washington, USA, August 4-10 (2001) (to appear)"},{"key":"35_CR29","doi-asserted-by":"crossref","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: Learning for quantified boolean logic satisfiability. In: The Eighteenth National Conference on Artificial Intelligence (AAAI 2002), Edmonton, Alberta, Canada, July 28-August 1 (2002)","DOI":"10.1016\/S0004-3702(02)00373-9"},{"key":"35_CR30","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-45616-3_12","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"R. Letz","year":"2002","unstructured":"Letz, R.: Lemma and model caching in decision procedures for quantified boolean formulas. In: Egly, U., Ferm\u00fcller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol.\u00a02381, pp. 160\u2013175. Springer, Heidelberg (2002)"},{"key":"35_CR31","series-title":"Lecture Notes in Computer Science","first-page":"348","volume-title":"Theory and Applications of Satisfiability Testing","author":"A.G.D. Rowley","year":"2004","unstructured":"Rowley, A.G.D., Gent, I., Giunchiglia, E., Narizzano, M., Tachella, A.: Watched data structures for QBF solvers. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 348\u2013355. Springer, Heidelberg (2004) (extended abstract)"},{"key":"35_CR32","unstructured":"Selman, B., Kautz, H.A., Cohen, B.: Noise strategies for improving local search. In: Proceedings of the Twelfth National Conference on Artificial Intelligence (AAAI 1994), Seattle, pp. 337\u2013343 (1994)"},{"issue":"3","key":"35_CR33","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1023\/A:1006249507577","volume":"24","author":"P. Balsiger","year":"2000","unstructured":"Balsiger, P., Heuerding, A., Schwendimann, S.: A benchmark method for the propositional modal logics k, kt, s4. Journal of Automated Reasoning\u00a024(3), 297\u2013317 (2000)","journal-title":"Journal of Automated Reasoning"},{"key":"35_CR34","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/S0004-3702(01)00113-8","volume":"131","author":"G. Sutcliff","year":"2001","unstructured":"Sutcliff, G., Suttner, C.: Evaluating general purpose automated theorem proving systems. Artificial Intelligence\u00a0131, 39\u201354 (2001)","journal-title":"Artificial Intelligence"},{"key":"35_CR35","unstructured":"Kautz, H.A., Selman, B.: Pushing the envelope: Planning, propositional logic, and stochastic search. In: Proceedings of the Twelfth National Conference on Artificial Intelligence (AAAI 1996), pp. 1194\u20131201 (1996)"},{"key":"35_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24605-3_35","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T23:54:20Z","timestamp":1559346860000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24605-3_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540208518","9783540246053"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24605-3_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}