Twelve Years of QBF Evaluations : QSAT Is PSPACE-Hard and It Shows

• Autorzy: Marin P. , Pulina L. , Giunchiglia E. , Narizzano M. , Tacchella A.

Identyfikatory

DOI

10.3233/FI-2016-1445

• Konferencja: Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion (22; 22.09.2015; Ferrara; Italy)
• Języki publikacji: EN

Abstrakty

EN

Twelve years have elapsed since the first Quantified Boolean Formulas (QBFs) evaluation was held as an event linked to SAT conferences. During this period, researchers have striven to propose new algorithms and tools to solve challenging formulas, with evaluations periodically trying to assess the current state of the art. In this paper, we present an experimental account of solvers and formulas with the aim to understand the progress in the QBF arena across these years. Unlike typical evaluations, the analysis is not confined to the snapshot of submitted solvers and formulas, but rather we consider several tools that were proposed over the last decade, and we run them on different formulas from previous QBF evaluations. The main contributions of our analysis, which are also the messages we would like to pass along to the research community, are: (i) many formulas that turned out to be difficult to solve in past evaluations, remain still challenging after twelve years, (ii) there is no single solver which can significantly outperform all the others, unless specific categories of formulas are considered, and (iii) effectiveness of preprocessing depends both on the coupled solver and the structure of the formula.

Słowa kluczowe

EN

computer algorithms; computational complexity; problem solving; mathematical formulas; machine theory

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2016
• Tom: Vol. 149, nr 1/2
• Strony: 133--158
• Opis fizyczny: Bibliogr. 38 poz., tab., wykr.

Twórcy

autor

Marin P.

• Lehrstuhl für Rechnerarchitektur, Georges-Köhler-Allee 051, 79110 Freiburg i.B., Germany

autor

Pulina L.

• POLCOMING, Università degli Studi di Sassari, Viale Mancini 5, 07100 Sassari, Italy

autor

Giunchiglia E.

• DIBRIS, Università degli Studi di Genova, Via Opera Pia 13, 16145 Genova, Italy

autor

Narizzano M.

• DIBRIS, Università degli Studi di Genova, Via Opera Pia 13, 16145 Genova, Italy

autor

Tacchella A.

• DIBRIS, Università degli Studi di Genova, Via Opera Pia 13, 16145 Genova, Italy

Bibliografia

• [1] Le Berre D, Simon L, Tacchella A. Challenges in the QBF arena: the SAT’03 evaluation of QBF solvers. In: Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT 2003). vol. 2919 of Lecture Notes in Computer Science. Springer Verlag; 2003. p. 468–485.
• [2] Peschiera C, Pulina L, Tacchella A, Bubeck U, Kullmann O, Lynce I. The seventh QBF solvers evaluation (QBFEVAL’10). In: Theory and Applications of Satisfiability Testing (SAT 2010). Springer Berlin Heidelberg; 2010. p. 237–250.
• [3] Lonsing F, Seidl M, Van Gelder A. QBF Gallery 2013; 2013. Available from: http://www.kr.tuwien.ac.at/events/qbfgallery2013/.
• [4] Janota M, Jordan C, Klieber W, Lonsing F, Seidl M. QBF Gallery 2014: The QBF Competition at the FLoC 2014 Olympic Games. Journal on Satisfiability, Boolean Modeling and Computation. 2016;9:187–206. Available from: https://satassociation.org/jsat/index.php/jsat/article/view/121/113.
• [5] Lonsing F, Seidl M, Van Gelder A. The QBF Gallery: Behind the scenes. Artificial Intelligence. 2016 08;237:92–114. Available from: http://www.sciencedirect.com/science/article/pii/S0004370216300376.
• [6] Pigorsch F, Scholl C. An AIG-based QBF-solver using SAT for preprocessing. In: Design Automation Conference (DAC), 2010 47th ACM/IEEE; 2010. p. 170–175.
• [7] Lonsing F, Biere A. DepQBF: A Dependency-Aware QBF Solver. Journal on Satisfiability, Boolean Modeling and Computation. 2010;7(2-3):71–76. Available from: http://jsat.ewi.tudelft.nl/content/volume7/JSAT7_6_Lonsing.pdf.
• [8] Klieber W, Sapra S, Gao S, Clarke E. A non-prenex, non-clausal QBF solver with game-state learning. In: Theory and Applications of Satisfiability Testing (SAT 2010). Springer; 2010. p. 128–142.
• [9] Biere A. Resolve and Expand. In: Seventh Intl. Conference on Theory and Applications of Satisfiability Testing (SAT’04). vol. 3542 of LNCS. Springer Verlag; 2005. p. 59–70.
• [10] Giunchiglia E, Marin P, Narizzano M. QuBE7.0. Journal on Satisfiability, Boolean Modeling and Computation. 2010;7(2-3):83–88. Available from: http://jsat.ewi.tudelft.nl/content/volume7/JSAT7_8_Giunchiglia.pdf.
• [11] Janota M, Klieber W, Marques-Silva J, Clarke E. Solving QBF with counterexample guided refinement. In: Theory and Applications of Satisfiability Testing (SAT 2012). Springer Berlin Heidelberg; 2012. p. 114–128.
• [12] Benedetti M. Evaluating QBFs via Symbolic Skolemization. In: Eleventh International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2004). vol. 3452 of Lecture Notes in Computer Science. Springer Verlag; 2004. p. 285–300.
• [13] Pulina L, Tacchella A. A structural approach to reasoning with quantified Boolean formulas. In: 21st International Joint Conference on Artificial Intelligence (IJCAI 2009); 2009. p. 596–602.
• [14] Pulina L, Tacchella A. A self-adaptive multi-engine solver for quantified Boolean formulas. Constraints. 2009;14(1):80–116.
• [15] Belov A, Diepold D, Heule MJH, Järvisalo M. Proceedings of SAT Competition 2014; Solver and Benchmark Descriptions. In: Department of Computer Science Series of Publications B. vol. B-2014-2. Helsinki: University of Helsinki; 2014. ISSN 1458-4786. Available from: https://tuhat.halvi.helsinki.fi/portal/files/40936166/sc2014_proceedings.pdf.
• [16] Barrett C, Deters M, de Moura L, Oliveras A, Stump A. 6 Years of SMT-COMP. Journal of Automated Reasoning. 2013;50(3):243–277.
• [17] Biere A, Lonsing F, Seidl M. Blocked Clause Elimination for QBF. In: Bjørner N, Sofronie-Stokkermans V, editors. Automated Deduction - 23rd International Conference on Automated Deduction (CADE-23), Wroclaw, Poland, July 31 - August 5, 2011. vol. 6803 of Lecture Notes in Computer Science. Springer; 2011. p. 101–115. Available from: http://dx.doi.org/10.1007/978-3-642-22438-6_10.
• [18] Heule M, Järvisalo M, Lonsing F, Seidl M, Biere A. Clause Elimination for SAT and QSAT. Journal of Artificial Intelligence Research (JAIR). 2015;53:127–168.
• [19] Giunchiglia E, Marin P, Narizzano M. sQueezeBF: An Effective Preprocessor for QBFs Based on Equivalence Reasoning. In: Strichman O, Szeider S, editors. 13th International Conference on Theory and Applications of Satisfiability Testing (SAT 2010), Edinburgh, UK, July 11-14, 2010. vol. 6175 of Lecture Notes in Computer Science. Springer; 2010. p. 85–98.
• [20] Lonsing F, Biere A. Failed Literal Detection for QBF. In: Sakallah K, Simon L, editors. Theory and Applications of Satisfiability Testing - SAT 2011. vol. 6695 of Lecture Notes in Computer Science. Springer Berlin Heidelberg; 2011. p. 259–272. Available from: http://dx.doi.org/10.1007/978-3-642-21581-0_21. doi:10.1007/978-3-642-21581-0_21.
• [21] Giunchiglia E, Narizzano M, Tacchella A. Clause-Term Resolution and Learning in Quantified Boolean Logic Satisfiability. Journal on Artificial Intelligence Research (JAIR). 2006;26:371–416.
• [22] Benedetti M. sKizzo: a Suite to Evaluate and Certify QBFs. In: 20th Int.l. Conference on Automated Deduction. vol. 3632 of LNCS. Springer Verlag; 2005. p. 369–376.
• [23] Pulina L, Tacchella A. Treewidth: a useful marker of empirical hardness in quantified Boolean logic encodings. In: 15th Int.l Conf. on Logic for Programming, Artificial Intelligence, and Reasoning. vol. 5330 of LNCS. Springer; 2008. p. 528–542.
• [24] Pulina L, Tacchella A. An empirical study of QBF encodings: from treewidth estimation to useful preprocessing. Fundamenta Informaticae. 2010;102(3):391–427.
• [25] Jordan C, Seidl M. The QBF Gallery 2014; 2014. Available from: http://qbf.satisfiability.org/gallery/qbf-gallery-2014-talk-long.pdf.
• [26] Plaisted DA, Greenbaum S. A Structure-preserving Clause Form Translation. Journal of Symbolic Computation. 1986;2:293–304.
• [27] Samulowitz H, Bacchus F. Binary clause reasoning in QBF. In: Nineth International Conference on Theory and Applications of Satisfiability Testing (SAT 2006). vol. 4121 of Lecture Notes in Computer Science. Springer; 2006. p. 353–367.
• [28] Bubeck U, Büning HK. Bounded Universal Expansion for Preprocessing QBF. In: Marques-Silva J, Sakallah KA, editors. 10th International Conference on Theory and Applications of Satisfiability Testing (SAT 2007), Lisbon, Portugal, May 28-31, 2007. Berlin, Heidelberg: Springer Berlin Heidelberg; 2007. p. 244–257.
• [29] Kronegger M, Pfandler A, Pichler R. Conformant planning as a benchmark for QBFsolvers. In: Intl. Workshop on Quantified Boolean Formulas (QBF 2013); 2013. p. 15. Available from: http://fmv.jku.at/qbf2013/reportQBFWS13.pdf.
• [30] Jordan C, Kaiser L. Experiments with Reduction Finding. In: Järvisalo M, Van Gelder A, editors. Theory and Applications of Satisfiability Testing (SAT 2013). vol. 7962 of Lecture Notes in Computer Science. Springer Berlin Heidelberg; 2013. p. 192–207.
• [31] Miller C, Scholl C, Becker B. Proving QBF-hardness in Bounded Model Checking for Incomplete Designs. In: 14th International Workshop on Microprocessor Test and Verification, MTV 2013, Austin, TX, USA, December 11-13, 2013. IEEE Computer Society; 2013. p. 23–28. Available from: http://dx.doi.org/10.1109/MTV.2013.11. doi:10.1109/MTV.2013.11.
• [32] Cashmore M, Fox M, Giunchiglia E. Partially Grounded Planning as Quantified Boolean Formula. In: Borrajo D, Kambhampati S, Oddi A, Fratini S, editors. Proceedings of the Twenty-Third International Conference on Automated Planning and Scheduling, (ICAPS 2013), Rome, Italy, June 10-14, 2013. AAAI; 2013. p. 26–32. Available from: http://www.aaai.org/ocs/index.php/ICAPS/ICAPS13/paper/view/5991.
• [33] Sauer M, Reimer S, Polian I, Schubert T, Becker B. Provably optimal test cube generation using quantified Boolean formula solving. In: Design Automation Conference (ASP-DAC), 2013 18th Asia and South Pacific; 2013. p. 533–539. doi:10.1109/ASPDAC.2013.6509651.
• [34] Narizzano M, Pulina L, Tacchella A. Report of the third QBF solvers evaluation. Journal on Satisfiability, Boolean Modeling and Computation. 2006;2:145–164.
• [35] Celeux G, Govaert G. A classification EM algorithm for clustering and two stochastic versions. Computational statistics & Data analysis. 1992;14(3):315–332.
• [36] Hall M, Frank E, Holmes G, Pfahringer B, Reutemann P, Witten IH. The WEKA data mining software: an update. ACM SIGKDD explorations newsletter. 2009;11(1):10–18.
• [37] Shapiro SS, Wilk MB. An analysis of variance test for normality (complete samples). Biometrika. 1965;52(3/4):591–611.
• [38] Quinlan JR. C4.5: programs for machine learning. Elsevier; 2014.

Uwagi

Opracowanie ze środków MNiSW w ramach umowy 812/P-DUN/2016 na działalność upowszechniającą naukę (zadania 2017).