×

zbMATH — the first resource for mathematics

The QBF Gallery: behind the scenes. (English) Zbl 1357.68209
Summary: Over the last few years, much progress has been made in the theory and practice of solving quantified Boolean formulas (QBF). Novel solvers have been presented that either successfully enhance established techniques or implement novel solving paradigms. Powerful preprocessors have been realized that tune the encoding of a formula to make it easier to solve. Frameworks for certification and solution extraction emerged that allow for a detailed interpretation of a QBF solver’s results, and new types of QBF encodings were presented for various application problems.
To capture these developments the QBF Gallery was established in 2013. The QBF Gallery aims at providing a forum to assess QBF tools and to collect new, expressive benchmarks that allow for documenting the status quo and that indicate promising research directions. These benchmarks became the basis for the experiments conducted in the context of the QBF Gallery 2013 and follow-up evaluations. In this paper, we report on the setup of the QBF Gallery. To this end, we conducted numerous experiments which allowed us not only to assess the quality of the tools, but also the quality of the benchmarks.

MSC:
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Balabanov, V.; Jiang, J. R., Unified QBF certification and its applications, Form. Methods Syst. Des., 41, 1, 45-65, (2012) · Zbl 1284.68516
[2] Balabanov, V.; Widl, M.; Jiang, J. R., QBF resolution systems and their proof complexities, (Proc. of the 17th Int. Conference on Theory and Applications of Satisfiability Testing, SAT, LNCS, vol. 8561, (2014), Springer), 154-169 · Zbl 1423.68406
[3] Benedetti, M.; Mangassarian, H., QBF-based formal verification: experience and perspectives, J. Satisf. Boolean Model. Comput., 5, 133-191, (2008) · Zbl 1172.68538
[4] Beyersdorff, O.; Chew, L.; Janota, M., On unification of QBF resolution-based calculi, (Proc. of the 39th Int. Symposium Mathematical Foundations of Computer Science, MFCS, LNCS, vol. 8635, (2014), Springer), 81-93 · Zbl 1426.68283
[5] Beyersdorff, O.; Chew, L.; Janota, M., Proof complexity of resolution-based QBF calculi, (Proc. of the 32nd Int. Symposium on Theoretical Aspects of Computer Science, STACS, LIPIcs, vol. 30, (2015), Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik), 76-89 · Zbl 1355.68105
[6] (Biere, A.; Heule, M.; van Maaren, H.; Walsh, T., Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, (2009), IOS Press) · Zbl 1183.68568
[7] Biere, A.; Lonsing, F.; Seidl, M., Blocked clause elimination for QBF, (Proc. of the 23rd Int. Conference on Automated Deduction, CADE, LNCS, vol. 6803, (2011), Springer), 101-115 · Zbl 1341.68181
[8] Bloem, R.; Könighofer, R.; Seidl, M., SAT-based synthesis methods for safety specs, (Proc. of the 15th Int. Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI, LNCS, vol. 8318, (2014), Springer), 1-20 · Zbl 1428.68040
[9] Brayton, R. K.; Mishchenko, A., ABC: an Academic industrial-strength verification tool, (Proc. of the 22nd Int. Conference on Computer Aided Verification, CAV, LNCS, vol. 6174, (2010), Springer), 24-40
[10] Cashmore, M.; Fox, M.; Giunchiglia, E., Planning as quantified Boolean formula, (Proc. of the 20th European Conference on Artificial Intelligence, ECAI, FAIA, vol. 242, (2012), IOS Press), 217-222 · Zbl 1327.68211
[11] Crouch, M.; Immerman, N.; Moss, J. Eliot B., Finding reductions automatically, (Fields of Logic and Computation, LNCS, vol. 6300, (2010), Springer), 181-200 · Zbl 1287.68024
[12] Egly, U.; Kronegger, M.; Lonsing, F.; Pfandler, A., Conformant planning as a case study of incremental QBF solving, (Proc. of the 12th Int. Conference on Artificial Intelligence and Symbolic Computation, AISC, LNCS, vol. 8884, (2014), Springer), 120-131
[13] Egly, U.; Lonsing, F.; Widl, M., Long-distance resolution: proof generation and strategy extraction in search-based QBF solving, (Proc. of the 19th Int. Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR, LNCS, vol. 8312, (2013), Springer), 291-308 · Zbl 1406.68106
[14] Giunchiglia, E.; Marin, P.; Narizzano, M., Qube7.0, J. Satisf. Boolean Model. Comput., 7, 2-3, 83-88, (2010)
[15] Giunchiglia, E.; Marin, P.; Narizzano, M., Squeezebf: an effective preprocessor for QBFs based on equivalence reasoning, (Proc. of the 13th Int. Conference on Theory and Applications of Satisfiability Testing, SAT, LNCS, vol. 6175, (2010), Springer), 85-98 · Zbl 1306.68157
[16] Giunchiglia, E.; Narizzano, M.; Tacchella, A., Quantified Boolean formulas satisfiability library, QBFLIB, (2001)
[17] Giunchiglia, E.; Narizzano, M.; Tacchella, A., Clause/term resolution and learning in the evaluation of quantified Boolean formulas, J. Artif. Intell. Res., 26, 371-416, (2006) · Zbl 1183.68475
[18] Goultiaeva, A.; Bacchus, F., Recovering and utilizing partial duality in QBF, (Proc. of the 16th Int. Conference on Theory and Applications of Satisfiability Testing, SAT, LNCS, vol. 7962, (2013), Springer), 83-99 · Zbl 1390.68573
[19] Goultiaeva, A.; Van Gelder, A.; Bacchus, F., A uniform approach for generating proofs and strategies for both true and false QBF formulas, (Proc. of the 22nd International Joint Conference on Artificial Intelligence, IJCAI, (2011), IJCAI/AAAI)
[20] Goultiaeva, A.; Seidl, M.; Biere, A., Bridging the gap between dual propagation and CNF-based QBF solving, (Design, Automation and Test in Europe, DATE, (2013), EDA Consortium San Jose/ACM DL), 811-814
[21] Heule, M.; Seidl, M.; Biere, A., A unified proof system for QBF preprocessing, (Proc. of the 7th Int. Joint Conference on Automated Reasoning, IJCAR, LNCS, vol. 8562, (2014), Springer), 91-106 · Zbl 1409.68257
[22] Janota, M.; Klieber, W.; Marques-Silva, J.; Clarke, E., Solving QBF with counterexample guided refinement, (Proc. of the 15th Int. Conference on Theory and Applications of Satisfiability Testing, SAT, LNCS, vol. 7317, (2012), Springer), 114-128 · Zbl 1273.68178
[23] Janota, M.; Marques-Silva, J., On propositional QBF expansions and Q-resolution, (Proc. of the 16th Int. Conference on Theory and Applications of Satisfiability Testing, SAT, LNCS, vol. 7962, (2013), Springer), 67-82 · Zbl 1390.03017
[24] Janota, M.; Marques-Silva, J., Expansion-based QBF solving versus Q-resolution, Theor. Comput. Sci., 577, 25-42, (2015) · Zbl 1309.68168
[25] Jordan, C.; Kaiser, L., Benchmarks from reduction finding, (QBF Workshop, (2013))
[26] Jordan, C.; Kaiser, L., Experiments with reduction finding, (Proc. of the 16th Int. Conference on Theory and Applications of Satisfiability Testing, SAT, LNCS, vol. 7962, (2013), Springer), 192-207 · Zbl 1390.68349
[27] Jussila, T.; Biere, A., Compressing BMC encodings with QBF, Electron. Notes Theor. Comput. Sci., 174, 3, 45-56, (2007) · Zbl 1277.68136
[28] Kleine Büning, H.; Bubeck, U., Theory of quantified Boolean formulas, (Handbook of Satisfiability, (2009), IOS Press), 735-760
[29] Kleine Büning, H.; Karpinski, M.; Flögel, A., Resolution for quantified Boolean formulas, Inf. Comput., 117, 1, 12-18, (1995) · Zbl 0828.68045
[30] Klieber, W.; Sapra, S.; Gao, S.; Clarke, E., A non-prenex, non-clausal QBF solver with game-state learning, (Proc. of the 13th Int. Conference on Theory and Applications of Satisfiability Testing, SAT, LNCS, vol. 6175, (2010), Springer), 128-142 · Zbl 1306.68161
[31] Kronegger, M.; Pfandler, A.; Pichler, R., Conformant planning as a benchmark for QBF-solvers, (QBF Workshop, (2013))
[32] Letz, R., Lemma and model caching in decision procedures for quantified Boolean formulas, (Proc. of the Int. Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX, LNCS, vol. 2381, (2002), Springer), 160-175 · Zbl 1015.68173
[33] Lindauer, M. T.; Hoos, H. H.; Hutter, F.; Schaub, T., Autofolio: an automatically configured algorithm selector, J. Artif. Intell. Res., 53, 745-778, (2015)
[34] Lonsing, F., Dependency schemes and search-based QBF solving: theory and practice, (2012), Johannes Kepler University Linz, Austria, PhD thesis
[35] Lonsing, F.; Biere, A., Failed literal detection for QBF, (Proc. of the 14th Int. Conference on Theory and Applications of Satisfiability Testing, SAT, LNCS, vol. 6695, (2011), Springer), 259-272 · Zbl 1330.68118
[36] Lonsing, F.; Egly, U.; Van Gelder, A., Efficient clause learning for quantified Boolean formulas via QBF pseudo unit propagation, (Proc. 16th Int. Conference on Theory and Applications of Satisfiability Testing, SAT, LNCS, vol. 7962, (2013)), 100-115 · Zbl 1390.68579
[37] Marin, P.; Narizzano, M.; Pulina, L.; Tacchella, A.; Giunchiglia, E., An empirical perspective on ten years of QBF solving, (Proc. of the 22nd RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion, RCRA 2015, CEUR Workshop Proceedings, vol. 1451, (2015), CEUR-WS.org), 62-75
[38] Miller, C.; Kupferschmid, S.; Lewis, M. D.T.; Becker, B., Encoding techniques, Craig interpolants and bounded model checking for incomplete designs, (Proc. of the 13th Int. Conference on Theory and Applications of Satisfiability Testing, SAT, LNCS, vol. 6175, (2010), Springer), 194-208 · Zbl 1306.68168
[39] Niemetz, A.; Preiner, M.; Lonsing, F.; Seidl, M.; Biere, A., Resolution-based certificate extraction for QBF - (tool presentation), (Proc. of the 15th Int. Conference on Theory and Applications of Satisfiability Testing, SAT, LNCS, vol. 7317, (2012), Springer), 430-435
[40] Peschiera, C.; Pulina, L.; Tacchella, A.; Bubeck, U.; Kullmann, O.; Lynce, I., The seventh QBF solvers evaluation (QBFEVAL’10), (Proc. of the 13th Int. Conference on Theory and Applications of Satisfiability Testing, SAT, LNCS, vol. 6175, (2010), Springer), 237-250 · Zbl 1306.68173
[41] Pulina, L.; Tacchella, A., Aqme’10, J. Satisf. Boolean Model. Comput., 7, 2-3, 65-70, (2010)
[42] Sauer, M.; Reimer, S.; Polian, I.; Schubert, T.; Becker, B., Provably optimal test cube generation using quantified Boolean formula solving, (Proc. of the 18th Asia and South Pacific Design Automation Conference, ASP-DAC, (2013), IEEE), 533-539
[43] Seidl, M.; Lonsing, F.; Van Gelder, A., QBF gallery 2013 (event website), (2013)
[44] Seidl, M.; Narizzano, M., The QBF evaluation 2012 - round 2, (2013)
[45] Van Gelder, A., Careful ranking of multiple solvers with timeouts and ties, (Proc. of the 14th Int. Conference on Theory and Applications of Satisfiability Testing, SAT, LNCS, vol. 6695, (2011), Springer), 317-328 · Zbl 1331.68213
[46] Van Gelder, A., Contributions to the theory of practical quantified Boolean formula solving, (Proc. of the 18th Int. Conference on Principles and Practice of Constraint Programming (CP), LNCS, vol. 7514, (2012), Springer), 647-663 · Zbl 1390.68585
[47] Van Gelder, A.; Wood, S. B.; Lonsing, F., Extended failed-literal preprocessing for quantified Boolean formulas, (Proc. of the 15th Int. Conference on Theory and Applications of Satisfiability Testing, SAT, LNCS, vol. 7317, (2012), Springer), 86-99 · Zbl 1273.68189
[48] Zhang, L.; Malik, S., Conflict driven learning in a quantified Boolean satisfiability solver, (Proc. of the 2002 IEEE/ACM International Conference on Computer-Aided Design, ICCAD, (2002), ACM), 442-449
[49] Zhang, L.; Malik, S., Towards a symmetric treatment of satisfaction and conflicts in quantified Boolean formula evaluation, (Proc. of the 8th Int. Conference on Principles and Practice of Constraint Programming (CP), LNCS, vol. 2470, (2002), Springer), 200-215
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.