Abstract
In this paper we report about QBFEVAL’10, the seventh in a series of events established with the aim of assessing the advancements in reasoning about quantified Boolean formulas (QBFs). The paper discusses the results obtained and the experimental setup, from the criteria used to select QBF instances to the evaluation infrastructure. We also discuss the current state-of-the-art in light of past challenges and we envision future research directions that are motivated by the results of QBFEVAL’10.
The authors would like to thank all the participants to the QBF competition and evaluations for submitting their work, and in particular Martina Seidl for her contribution related to the input format of non-prenex non-CNF formulas.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Le Berre, D., Roussel, O., Simon, L.: The SAT 2009 Competition (2009), www.satcompetition.org/2009
Sinz, C.: Sat-race (2008), baldur.iti.uka.de/sat-race-2008
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)
Long, D., Fox, M.: The 3rd International Planning Competition: Results and Analysis. Artificial Intelligence Research 20, 1–59 (2003)
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–841 (2009)
Le Berre, D., Simon, L., Tacchella, A.: Challenges in the QBF arena: the SAT’03 evaluation of QBF solvers. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 468–485. Springer, Heidelberg (2004)
Narizzano, M., Pulina, L., Tacchella, A.: Ranking and Reputation Sytems in the QBF competition. In: Proc. of AI*IA 2007, pp. 97–108 (2007)
Pigorsch, F., Scholl, C.: Exploiting structure in an aig based qbf solver. In: Proc. of DATE 2009, pp. 1596–1601 (2009)
Pulina, L., Tacchella, A.: A self-adaptive multi-engine solver for quantified Boolean formulas. Constraints 14(1), 80–116 (2009)
Goultiaeva, A., Iverson, V., Bacchus, F.: Beyond CNF: A Circuit-Based QBF Solver. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 412–426. Springer, Heidelberg (2009)
Lonsing, F., Biere, A.: Efficiently Representing Existential Dependency Sets for Expansion-based QBF Solvers. Electronic Notes in Theoretical Computer Science 251, 83–95 (2009)
Lonsing, F., Biere, A.: Nenofex: Expanding nnf for qbf solving. In: Kleine Büning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol. 4996, pp. 196–210. Springer, Heidelberg (2008)
Lewis, M., Schubert, T., Becker, B.: QMiraXT–A Multithreaded QBF Solver. In: Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (2009)
Egly, U., Seidl, M., Woltran, S.: A solver for QBFs in negation normal form. Constraints 14(1), 38–79 (2009)
Biere, A.: Resolve and Expand. In: Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 59–70. Springer, Heidelberg (2005)
Giunchiglia, E., Marin, P., Narizzano, M.: Preprocessing Techniques for QBFs. In: Proc. of 15th RCRA workshop (2008)
Giunchiglia, E., Narizzano, M., Tacchella, A.: Clause-Term Resolution and Learning in Quantified Boolean Logic Satisfiability. Artificial Intelligence Research 26, 371–416 (2006)
Pulina, L., Tacchella, A.: A structural approach to reasoning with quantified Boolean formulas. In: Proc. of IJCAI 2009, pp. 596–602 (2009)
Peschiera, C., Pulina, L., Tacchella, A.: Seventh QBF solvers evaluation, QBFEVAL (2010), http://www.qbfeval.org/2010
Giunchiglia, E., Narizzano, M., Pulina, L., Tacchella, A.: Quantified Boolean Formulas satisfiability library, QBFLIB (2001), http://www.qbflib.org
Cook, B., Kroening, D., Rümmer, P., Wintersteiger, C.M.: Ranking function synthesis for bit-vector relations. In: Proc. of TACAS 2010 (to appear, 2010)
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. 5330, pp. 528–542. Springer, Heidelberg (2008)
Chen, H., Interian, Y.: A Model for Generating Random Quantified Boolean Formulas. In: Proc. of IJCAI 2005, pp. 66–71 (2005)
Yu, Y., Malik, S.: Verifying the Correctness of Quantified Boolean Formula(QBF) Solvers: Theory and Practice. In: Proc. of ASP-DAC 2005, pp. 1047–1051 (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Peschiera, C., Pulina, L., Tacchella, A., Bubeck, U., Kullmann, O., Lynce, I. (2010). The Seventh QBF Solvers Evaluation (QBFEVAL’10). In: Strichman, O., Szeider, S. (eds) Theory and Applications of Satisfiability Testing – SAT 2010. SAT 2010. Lecture Notes in Computer Science, vol 6175. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14186-7_20
Download citation
DOI: https://doi.org/10.1007/978-3-642-14186-7_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14185-0
Online ISBN: 978-3-642-14186-7
eBook Packages: Computer ScienceComputer Science (R0)