Advertisement

Evaluating QBF Solvers: Quantifier Alternations Matter

  • Florian LonsingEmail author
  • Uwe EglyEmail author
Conference paper
First Online:
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11008)

Abstract

We present an experimental study of the effects of quantifier alternations on the evaluation of quantified Boolean formula (QBF) solvers. The number of quantifier alternations in a QBF in prenex conjunctive normal form (PCNF) is directly related to the theoretical hardness of the respective QBF satisfiability problem in the polynomial hierarchy. We show empirically that the performance of solvers based on different solving paradigms substantially varies depending on the numbers of alternations in PCNFs. In related theoretical work, quantifier alternations have become the focus of understanding the strengths and weaknesses of various QBF proof systems implemented in solvers. Our results motivate the development of methods to evaluate orthogonal solving paradigms by taking quantifier alternations into account. This is necessary to showcase the broad range of existing QBF solving paradigms for practical QBF applications. Moreover, we highlight the potential of combining different approaches and QBF proof systems in solvers.

This is a preview of subscription content, log in to check access.

References

  1. 1.
    Atserias, A., Oliva, S.: Bounded-width QBF is PSPACE-complete. In: STACS. LIPIcs, vol. 20, pp. 44–54. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2013)Google Scholar
  2. 2.
    Ayari, A., Basin, D.: Qubos: deciding quantified boolean logic using propositional satisfiability solvers. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 187–201. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-36126-X_12CrossRefGoogle Scholar
  3. 3.
    Balint, A., Belov, A., Järvisalo, M., Sinz, C.: Overview and analysis of the SAT challenge 2012 solver competition. Artif. Intell. 223, 120–155 (2015)CrossRefGoogle Scholar
  4. 4.
    Balyo, T., Biere, A., Iser, M., Sinz, C.: SAT race 2015. Artif. Intell. 241, 45–65 (2016).  https://doi.org/10.1016/j.artint.2016.08.007MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Balyo, T., Heule, M.J.H., Järvisalo, M.: SAT competition 2016: recent developments. In: AAAI, pp. 5061–5063. AAAI Press (2017)Google Scholar
  6. 6.
    Beyersdorff, O., Blinkhorn, J., Hinde, L.: Size, cost and capacity: a semantic technique for hard random QBFs. In: ITCS. LIPIcs, vol. 94, pp. 9:1–9:18. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2018)Google Scholar
  7. 7.
    Beyersdorff, O., Chew, L., Janota, M.: Proof complexity of resolution-based QBF calculi. In: STACS. LIPIcs, vol. 30, pp. 76–89. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015)Google Scholar
  8. 8.
    Beyersdorff, O., Chew, L., Janota, M.: Extension variables in QBF Resolution. In: Beyond NP Workshop, AAAI Workshops, vol. WS-16-05. AAAI Press (2016)Google Scholar
  9. 9.
    Beyersdorff, O., Hinde, L., Pich, J.: Reasons for hardness in QBF proof systems. In: FSTTCS. LIPIcs, vol. 93, pp. 14:1–14:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2017)Google Scholar
  10. 10.
    Biere, A.: Resolve and expand. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 59–70. Springer, Heidelberg (2005).  https://doi.org/10.1007/11527695_5CrossRefzbMATHGoogle Scholar
  11. 11.
    Bogaerts, B., Janhunen, T., Tasharrofi, S.: SAT-to-SAT in QBFEval 2016. In: QBF Workshop, CEUR Workshop Proceedings, vol. 1719, pp. 63–70. CEUR-WS.org (2016)Google Scholar
  12. 12.
    Bogaerts, B., Janhunen, T., Tasharrofi, S.: Solving QBF instances with nested SAT solvers. In: Beyond NP Workshop 2016 at AAAI 2016 (2016)Google Scholar
  13. 13.
    Bordeaux, L., Cadoli, M., Mancini, T.: CSP properties for quantified constraints: definitions and complexity. In: AAAI, pp. 360–365. AAAI Press/The MIT Press (2005)Google Scholar
  14. 14.
    Cadoli, M., Giovanardi, A., Schaerf, M.: An algorithm to evaluate quantified Boolean formulae. In: AAAI, pp. 262–267. AAAI Press/The MIT Press (1998)Google Scholar
  15. 15.
    Charwat, G., Woltran, S.: Expansion-based QBF solving on tree decompositions. In: RCRA Workshop, CEUR Workshop Proceedings, vol. 2011, pp. 16–26. CEUR-WS.org (2017)Google Scholar
  16. 16.
    Chen, H.: A rendezvous of logic, complexity, and algebra. ACM Comput. Surv. 42(1), 2:1–2:32 (2009)CrossRefGoogle Scholar
  17. 17.
    Chen, H.: Meditations on quantified constraint satisfaction. In: Constable, R.L., Silva, A. (eds.) Logic and Program Semantics. LNCS, vol. 7230, pp. 35–49. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-29485-3_4CrossRefGoogle Scholar
  18. 18.
    Chen, H.: Proof complexity modulo the polynomial hierarchy: understanding alternation as a source of hardness. TOCT 9(3), 15:1–15:20 (2017)MathSciNetGoogle Scholar
  19. 19.
    Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752–794 (2003)MathSciNetCrossRefGoogle Scholar
  20. 20.
    Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symb. Log. 44(1), 36–50 (1979)MathSciNetCrossRefGoogle Scholar
  21. 21.
    Davis, M., Logemann, G., Loveland, D.W.: A machine program for theorem-proving. Commun. ACM 5(7), 394–397 (1962)MathSciNetCrossRefGoogle Scholar
  22. 22.
    Egly, U., Seidl, M., Tompits, H., Woltran, S., Zolda, M.: Comparing different prenexing strategies for quantified Boolean formulas. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 214–228. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-24605-3_17CrossRefGoogle Scholar
  23. 23.
    Giunchiglia, E., Narizzano, M., Pulina, L., Tacchella, A.: Quantified Boolean Formulas Library (QBFLIB) and Solver Evaluation Portal (QBFEVAL) (2004). www.qbflib.org
  24. 24.
    Giunchiglia, E., Narizzano, M., Tacchella, A.: Learning for quantified boolean logic satisfiability. In: AAAI, pp. 649–654. AAAI Press/The MIT Press (2002)Google Scholar
  25. 25.
    Giunchiglia, E., Narizzano, M., Tacchella, A.: Clause/term resolution and learning in the evaluation of quantified Boolean formulas. JAIR 26, 371–416 (2006)MathSciNetCrossRefGoogle Scholar
  26. 26.
    Heule, M., Järvisalo, M., Lonsing, F., Seidl, M., Biere, A.: Clause elimination for SAT and QSAT. JAIR 53, 127–168 (2015)MathSciNetCrossRefGoogle Scholar
  27. 27.
    Hooker, J.N.: Testing heuristics: we have it all wrong. J. Heuristics 1(1), 33–42 (1995)CrossRefGoogle Scholar
  28. 28.
    Janota, M.: Towards generalization in QBF solving via machine learning. In: Proceedings of the AAAI 2018 (2018, to appear)Google Scholar
  29. 29.
    Janota, M., Jordan, C., Klieber, W., Lonsing, F., Seidl, M., Van Gelder, A.: The QBFGallery 2014: the QBF competition at the FLoC olympic games. JSAT 9, 187–206 (2016)Google Scholar
  30. 30.
    Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.: Solving QBF with counterexample guided refinement. Artif. Intell. 234, 1–25 (2016)MathSciNetCrossRefGoogle Scholar
  31. 31.
    Janota, M., Marques-Silva, J.: Expansion-based QBF solving versus Q-resolution. Theor. Comput. Sci. 577, 25–42 (2015)MathSciNetCrossRefGoogle Scholar
  32. 32.
    Janota, M., Marques-Silva, J.: Solving QBF by clause selection. In: IJCAI, pp. 325–331. AAAI Press (2015)Google Scholar
  33. 33.
    Kleine Büning, H., Bubeck, U.: Theory of quantified Boolean formulas. In: Handbook of Satisfiability, FAIA, vol. 185, pp. 735–760. IOS Press (2009)Google Scholar
  34. 34.
    Kleine Büning, H., Karpinski, M., Flögel, A.: Resolution for quantified Boolean formulas. Inf. Comput. 117(1), 12–18 (1995)MathSciNetCrossRefGoogle Scholar
  35. 35.
    Klieber, W., Sapra, S., Gao, S., Clarke, E.: A non-prenex, non-clausal QBF solver with game-state learning. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 128–142. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-14186-7_12CrossRefGoogle Scholar
  36. 36.
    Letz, R.: Lemma and model caching in decision procedures for quantified Boolean formulas. In: Egly, U., Fermüller, C.G. (eds.) TABLEAUX 2002. LNCS (LNAI), vol. 2381, pp. 160–175. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-45616-3_12CrossRefzbMATHGoogle Scholar
  37. 37.
    Lonsing, F., Egly, U.: DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 371–384. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-63046-5_23CrossRefGoogle Scholar
  38. 38.
    Lonsing, F., Egly, U.: Evaluating QBF solvers: quantifier alternations matter. CoRR abs/1701.06612 (2018). http://arxiv.org/abs/1701.06612, CP 2018 proceedings version with appendix
  39. 39.
    Lonsing, F., Seidl, M., Van Gelder, A.: The QBF gallery: behind the scenes. Artif. Intell. 237, 92–114 (2016)MathSciNetCrossRefGoogle Scholar
  40. 40.
    Marin, P., Narizzano, M., Pulina, L., Tacchella, A., Giunchiglia, E.: Twelve years of QBF evaluations: QSAT is PSPACE-hard and it shows. Fundam. Inf. 149(1–2), 133–158 (2016)MathSciNetCrossRefGoogle Scholar
  41. 41.
    Martin, B.: Quantified constraints in twenty seventeen. In: The Constraint Satisfaction Problem: Complexity and Approximability, Dagstuhl Follow-Ups, vol. 7, pp. 327–346. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2017)Google Scholar
  42. 42.
    Meyer, A.R., Stockmeyer, L.J.: The equivalence problem for regular expressions with squaring requires exponential space. In: 13th Annual Symposium on Switching and Automata Theory, pp. 125–129. IEEE Computer Society (1972)Google Scholar
  43. 43.
    Peitl, T., Slivovsky, F., Szeider, S.: Dependency learning for QBF. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 298–313. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-66263-3_19CrossRefGoogle Scholar
  44. 44.
    Pulina, L., Seidl, M.: QBFEVAL’17: competitive evaluation of QBF solvers (2017). http://www.qbflib.org/event_page.php?year=2017
  45. 45.
    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).  https://doi.org/10.1007/978-3-540-89439-1_37CrossRefzbMATHGoogle Scholar
  46. 46.
    Rabe, M.N., Tentrup, L.: CAQE: a certifying QBF solver. In: FMCAD, pp. 136–143. IEEE (2015)Google Scholar
  47. 47.
    Silva, J.P.M., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Handbook of Satisfiability, FAIA, vol. 185, pp. 131–153. IOS Press (2009)Google Scholar
  48. 48.
    Stockmeyer, L.J.: The polynomial-time hierarchy. Theor. Comput. Sci. 3(1), 1–22 (1976)MathSciNetCrossRefGoogle Scholar
  49. 49.
    Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time: preliminary report. In: STOC, pp. 1–9. ACM (1973)Google Scholar
  50. 50.
    Tentrup, L.: On expansion and resolution in CEGAR based QBF solving. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 475–494. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-63390-9_25CrossRefGoogle Scholar
  51. 51.
    Tseitin, G.S.: On the complexity of derivation in propositional calculus. Stud. Constr. Math. Math. Log., 115–125 (1968)Google Scholar
  52. 52.
    Wimmer, R., Reimer, S., Marin, P., Becker, B.: HQSpre – an effective preprocessor for QBF and DQBF. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 373–390. Springer, Heidelberg (2017).  https://doi.org/10.1007/978-3-662-54577-5_21CrossRefGoogle Scholar
  53. 53.
    Wrathall, C.: Complete sets and the polynomial-time hierarchy. Theor. Comput. Sci. 3(1), 23–33 (1976)MathSciNetCrossRefGoogle Scholar
  54. 54.
    Xu, L., Hutter, F., Hoos, H., Leyton-Brown, K.: Evaluating component solver contributions to portfolio-based algorithm selectors. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 228–241. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-31612-8_18CrossRefGoogle Scholar
  55. 55.
    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. 2470, pp. 200–215. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-46135-3_14CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Research Division of Knowledge Based Systems, Institute of Logic and ComputationTU WienViennaAustria

Personalised recommendations

Cite paper

Buy options