Skip to main content
SpringerLink
Log in
Book cover

International Conference on Principles and Practice of Constraint Programming

CP 2018: Principles and Practice of Constraint Programming pp 195–209Cite as

Portfolio-Based Algorithm Selection for Circuit QBFs

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11008))

Abstract

Quantified Boolean Formulas (QBFs) are a generalization of propositional formulae that admits succinct encodings of verification and synthesis problems. Given that modern QBF solvers are based on different architectures with complementary performance characteristics, a portfolio-based approach to QBF solving is particularly promising.

While general QBFs can be converted to prenex conjunctive normal form (PCNF) with small overhead, this transformation has been known to adversely affect performance. This issue has prompted the development of several solvers for circuit QBFs in recent years.

We define a natural set of features of circuit QBFs and show that they can be used to construct portfolio-based algorithm selectors of state-of-the-art circuit QBF solvers that are close to the virtual best solver. We further demonstrate that most of this performance can be achieved using surprisingly small subsets of cheaply computable and intuitive features.

This research was partially supported by FWF grants P27721 and W1255-N23.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    We only consider “cleansed” QCIR instances in prenex normal form supported by the current generation of solvers.

  2. 2.

    See http://www.qbflib.org.

References

  1. Ansótegui, C., Gomes, C.P., Selman, B.: The Achilles’ heel of QBF. In: Veloso, M.M., Kambhampati, S. (eds.) The Twentieth National Conference on Artificial Intelligence - AAAI 2005, pp. 275–281. AAAI Press/The MIT Press (2005)

    Google Scholar 

  2. Balyo, T., Lonsing, F.: HordeQBF: a modular and massively parallel QBF solver. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 531–538. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40970-2_33

    Chapter  MATH  Google Scholar 

  3. Beyersdorff, O., Chew, L., Janota, M.: Proof complexity of resolution-based QBF calculi. In: Mayr, E.W., Ollinger, N. (eds.) 32nd International Symposium on Theoretical Aspects of Computer Science, STACS 2015, 4–7 March 2015, Garching, Germany. LIPIcs, vol. 30, pp. 76–89. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015)

    Google Scholar 

  4. Biere, A.: Bounded model checking. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 457–481. IOS Press (2009)

    Google Scholar 

  5. Gebser, M., et al.: A portfolio solver for answer set programming: preliminary report. In: Delgrande, J.P., Faber, W. (eds.) LPNMR 2011. LNCS (LNAI), vol. 6645, pp. 352–357. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-20895-9_40

    Chapter  Google Scholar 

  6. Hutter, F., Hoos, H.H., Leyton-Brown, K.: Sequential model-based optimization for general algorithm configuration. In: Coello, C.A.C. (ed.) LION 2011. LNCS, vol. 6683, pp. 507–523. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-25566-3_40

    Chapter  Google Scholar 

  7. Hutter, F., Hoos, H.H., Leyton-Brown, K., Stützle, T.: Paramils: an automatic algorithm configuration framework. J. Artif. Intell. Res. 36, 267–306 (2009)

    Article  Google Scholar 

  8. Janota, M.: Towards generalization in QBF solving via machine learning. In: McIlraith, S.A., Weinberger, K.Q. (eds.) Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence - AAAI 2018. AAAI Press (2018)

    Google Scholar 

  9. Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.: Solving QBF with counterexample guided refinement. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 114–128. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31612-8_10

    Chapter  Google Scholar 

  10. Janota, M., Marques-Silva, J.: Expansion-based QBF solving versus Q-resolution. Theor. Comput. Sci. 577, 25–42 (2015)

    Article  MathSciNet  Google Scholar 

  11. Janota, M., Marques-Silva, J.: Solving QBF by clause selection. In: Yang, Q., Wooldridge, M. (eds.) Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015. pp. 325–331. AAAI Press (2015)

    Google Scholar 

  12. Jordan, C., Klieber, W., Seidl, M.: Non-CNF QBF solving with QCIR. In: Darwiche, A. (ed.) Beyond NP, Papers from the 2016 AAAI Workshop, Phoenix, Arizona, USA, February 12, 2016. AAAI Workshops, vol. WS-16-05. AAAI Press (2016)

    Google Scholar 

  13. 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_12

    Chapter  Google Scholar 

  14. Kotthoff, L.: Algorithm selection for combinatorial search problems: a survey. In: Bessiere, C., et al. (eds.) Data Mining and Constraint Programming. LNCS (LNAI), vol. 10101, pp. 149–190. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-50137-6_7

    Chapter  Google Scholar 

  15. Lindauer, M.T., Hoos, H.H., Hutter, F., Schaub, T.: Autofolio: an automatically configured algorithm selector. J. Artif. Intell. Res. 53, 745–778 (2015)

    Article  Google Scholar 

  16. 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_23

    Chapter  Google Scholar 

  17. Lonsing, F., Egly, U.: Evaluating QBF solvers: quantifier alternations matter. CoRR abs/1701.06612 (2017). http://arxiv.org/abs/1701.06612

  18. O’Mahony, E., Hebrard, E., Holland, A., Nugent, C., O’Sullivan, B.: Using case-based reasoning in an algorithm portfolio for constraint solving. In: Irish Conference on Artificial Intelligence and Cognitive Science, pp. 210–216 (2008)

    Google Scholar 

  19. 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_19

    Chapter  Google Scholar 

  20. Pulina, L., Tacchella, A.: A self-adaptive multi-engine solver for quantified Boolean formulas. Constraints 14(1), 80–116 (2009)

    Article  MathSciNet  Google Scholar 

  21. Rabe, M.N., Tentrup, L.: CAQE: a certifying QBF solver. In: Kaivola, R., Wahl, T. (eds.) Formal Methods in Computer-Aided Design - FMCAD 2015, pp. 136–143. IEEE Computer Society (2015)

    Google Scholar 

  22. Rice, J.R.: The algorithm selection problem. Adv. Comput. 15, 65–118 (1976)

    Article  Google Scholar 

  23. Rintanen, J.: Planning and SAT. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 483–504. IOS Press (2009)

    Google Scholar 

  24. Samulowitz, H., Memisevic, R.: Learning to solve QBF. In: Proceedings of the Twenty-Second AAAI Conference on Artificial Intelligence, July 22–26, 2007, Vancouver, British Columbia, Canada, pp. 255–260. AAAI Press (2007)

    Google Scholar 

  25. Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time: preliminary report. In: Aho, A.V., et al. (eds.) Proceedings of the 5th Annual ACM Symposium on Theory of Computing, 30 April–2 May 1973, Austin, Texas, USA, pp. 1–9. Association for Computing Machinery, New York (1973)

    Google Scholar 

  26. Tentrup, L.: Non-prenex QBF solving using abstraction. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 393–401. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40970-2_24

    Chapter  Google Scholar 

  27. Vizel, Y., Weissenbacher, G., Malik, S.: Boolean satisfiability solvers and their applications in model checking. Proc. IEEE 103(11), 2021–2035 (2015)

    Article  Google Scholar 

  28. Xu, L., Hoos, H., Leyton-Brown, K.: Hydra: automatically configuring algorithms for portfolio-based selection. In: Fox, M., Poole, D. (eds.) Proceedings of the Twenty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2010, Atlanta, Georgia, USA, 11–15 July 2010. AAAI Press (2010)

    Google Scholar 

  29. Xu, L., Hutter, F., Hoos, H.H., Leyton-Brown, K.: Satzilla: portfolio-based algorithm selection for SAT. J. Artif. Intell. Res. 32, 565–606 (2008)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Leiden Institute of Advanced Computer Science, Leiden University, Leiden, The Netherlands

    Holger H. Hoos

  2. Algorithms and Complexity Group, TU Wien, Vienna, Austria

    Tomáš Peitl, Friedrich Slivovsky & Stefan Szeider

Authors
  1. Holger H. Hoos
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Tomáš Peitl
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Friedrich Slivovsky
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Stefan Szeider
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Tomáš Peitl .

Editor information

Editors and Affiliations

  1. Carnegie Mellon University, Pittsburgh, PA, USA

    John Hooker

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Hoos, H.H., Peitl, T., Slivovsky, F., Szeider, S. (2018). Portfolio-Based Algorithm Selection for Circuit QBFs. In: Hooker, J. (eds) Principles and Practice of Constraint Programming. CP 2018. Lecture Notes in Computer Science(), vol 11008. Springer, Cham. https://doi.org/10.1007/978-3-319-98334-9_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-98334-9_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-98333-2

  • Online ISBN: 978-3-319-98334-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation