{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:55:59Z","timestamp":1725558959413},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642141850"},{"type":"electronic","value":"9783642141867"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14186-7_20","type":"book-chapter","created":{"date-parts":[[2010,7,8]],"date-time":"2010-07-08T22:20:37Z","timestamp":1278627637000},"page":"237-250","source":"Crossref","is-referenced-by-count":11,"title":["The Seventh QBF Solvers Evaluation (QBFEVAL\u201910)"],"prefix":"10.1007","author":[{"given":"Claudia","family":"Peschiera","sequence":"first","affiliation":[]},{"given":"Luca","family":"Pulina","sequence":"additional","affiliation":[]},{"given":"Armando","family":"Tacchella","sequence":"additional","affiliation":[]},{"given":"Uwe","family":"Bubeck","sequence":"additional","affiliation":[]},{"given":"Oliver","family":"Kullmann","sequence":"additional","affiliation":[]},{"given":"In\u00eas","family":"Lynce","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","unstructured":"Le Berre, D., Roussel, O., Simon, L.: The SAT 2009 Competition (2009), www.satcompetition.org\/2009"},{"key":"20_CR2","unstructured":"Sinz, C.: Sat-race (2008), baldur.iti.uka.de\/sat-race-2008"},{"key":"20_CR3","unstructured":"Barrett, C., Deters, M., Oliveras, A., Stump, A.: Design and results of the 4th annual satisfiability modulo theories competition (SMT-COMP 2008) (to appear, 2008)"},{"key":"20_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1023\/A:1026044009832","volume":"20","author":"D. Long","year":"2003","unstructured":"Long, D., Fox, M.: The 3rd International Planning Competition: Results and Analysis. Artificial Intelligence Research\u00a020, 1\u201359 (2003)","journal-title":"Artificial Intelligence Research"},{"key":"20_CR5","unstructured":"Kontchakov, R., Pulina, L., Sattler, U., Schneider, T., Selmer, P., Wolter, F., Zakharyaschev, M.: Minimal Module Extraction from DL-Lite Ontologies using QBF Solvers. In: Proc. of IJCAI 2009, pp. 836\u2013841 (2009)"},{"key":"20_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"468","DOI":"10.1007\/978-3-540-24605-3_35","volume-title":"Theory and Applications of Satisfiability Testing","author":"D. Berre Le","year":"2004","unstructured":"Le Berre, D., Simon, L., Tacchella, A.: Challenges in the QBF arena: the SAT\u201903 evaluation of QBF solvers. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 468\u2013485. Springer, Heidelberg (2004)"},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"Narizzano, M., Pulina, L., Tacchella, A.: Ranking and Reputation Sytems in the QBF competition. In: Proc. of AI*IA 2007, pp. 97\u2013108 (2007)","DOI":"10.1007\/978-3-540-74782-6_10"},{"key":"20_CR8","doi-asserted-by":"crossref","unstructured":"Pigorsch, F., Scholl, C.: Exploiting structure in an aig based qbf solver. In: Proc. of DATE 2009, pp. 1596\u20131601 (2009)","DOI":"10.1109\/DATE.2009.5090919"},{"issue":"1","key":"20_CR9","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/s10601-008-9051-2","volume":"14","author":"L. Pulina","year":"2009","unstructured":"Pulina, L., Tacchella, A.: A self-adaptive multi-engine solver for quantified Boolean formulas. Constraints\u00a014(1), 80\u2013116 (2009)","journal-title":"Constraints"},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1007\/978-3-642-02777-2_38","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"A. Goultiaeva","year":"2009","unstructured":"Goultiaeva, A., Iverson, V., Bacchus, F.: Beyond CNF: A Circuit-Based QBF Solver. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 412\u2013426. Springer, Heidelberg (2009)"},{"key":"20_CR11","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/j.entcs.2009.08.029","volume":"251","author":"F. Lonsing","year":"2009","unstructured":"Lonsing, F., Biere, A.: Efficiently Representing Existential Dependency Sets for Expansion-based QBF Solvers. Electronic Notes in Theoretical Computer Science\u00a0251, 83\u201395 (2009)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"20_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/978-3-540-79719-7_19","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2008","author":"F. Lonsing","year":"2008","unstructured":"Lonsing, F., Biere, A.: Nenofex: Expanding nnf for qbf solving. In: Kleine B\u00fcning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol.\u00a04996, pp. 196\u2013210. Springer, Heidelberg (2008)"},{"key":"20_CR13","unstructured":"Lewis, M., Schubert, T., Becker, B.: QMiraXT\u2013A Multithreaded QBF Solver. In: Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (2009)"},{"issue":"1","key":"20_CR14","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/s10601-008-9055-y","volume":"14","author":"U. Egly","year":"2009","unstructured":"Egly, U., Seidl, M., Woltran, S.: A solver for QBFs in negation normal form. Constraints\u00a014(1), 38\u201379 (2009)","journal-title":"Constraints"},{"key":"20_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/11527695_5","volume-title":"Theory and Applications of Satisfiability Testing","author":"A. Biere","year":"2005","unstructured":"Biere, A.: Resolve and Expand. In: Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 59\u201370. Springer, Heidelberg (2005)"},{"key":"20_CR16","unstructured":"Giunchiglia, E., Marin, P., Narizzano, M.: Preprocessing Techniques for QBFs. In: Proc. of 15th RCRA workshop (2008)"},{"key":"20_CR17","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1613\/jair.1959","volume":"26","author":"E. Giunchiglia","year":"2006","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: Clause-Term Resolution and Learning in Quantified Boolean Logic Satisfiability. Artificial Intelligence Research\u00a026, 371\u2013416 (2006)","journal-title":"Artificial Intelligence Research"},{"key":"20_CR18","unstructured":"Pulina, L., Tacchella, A.: A structural approach to reasoning with quantified Boolean formulas. In: Proc. of IJCAI 2009, pp. 596\u2013602 (2009)"},{"key":"20_CR19","unstructured":"Peschiera, C., Pulina, L., Tacchella, A.: Seventh QBF solvers evaluation, QBFEVAL (2010), http:\/\/www.qbfeval.org\/2010"},{"key":"20_CR20","unstructured":"Giunchiglia, E., Narizzano, M., Pulina, L., Tacchella, A.: Quantified Boolean Formulas satisfiability library, QBFLIB (2001), http:\/\/www.qbflib.org"},{"key":"20_CR21","unstructured":"Cook, B., Kroening, D., R\u00fcmmer, P., Wintersteiger, C.M.: Ranking function synthesis for bit-vector relations. In: Proc. of TACAS 2010 (to appear, 2010)"},{"key":"20_CR22","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"528","DOI":"10.1007\/978-3-540-89439-1_37","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"L. Pulina","year":"2008","unstructured":"Pulina, L., Tacchella, A.: Treewidth: a useful marker of empirical hardness in quantified Boolean logic encodings. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol.\u00a05330, pp. 528\u2013542. Springer, Heidelberg (2008)"},{"key":"20_CR23","doi-asserted-by":"crossref","unstructured":"Chen, H., Interian, Y.: A Model for Generating Random Quantified Boolean Formulas. In: Proc. of IJCAI 2005, pp. 66\u201371 (2005)","DOI":"10.1007\/11527695_6"},{"key":"20_CR24","doi-asserted-by":"crossref","unstructured":"Yu, Y., Malik, S.: Verifying the Correctness of Quantified Boolean Formula(QBF) Solvers: Theory and Practice. In: Proc. of ASP-DAC 2005, pp. 1047\u20131051 (2005)","DOI":"10.1145\/1120725.1120821"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2010"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14186-7_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T22:31:29Z","timestamp":1559255489000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14186-7_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642141850","9783642141867"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14186-7_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}