Skip to main content
SpringerLink
Log in

Robust Benchmark Set Selection for Boolean Constraint Solvers

  • Conference paper
  • First Online:
Learning and Intelligent Optimization (LION 2013)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7997))

Included in the following conference series:

Abstract

We investigate the composition of representative benchmark sets for evaluating and improving the performance of robust Boolean constraint solvers in the context of satisfiability testing and answer set programming. Starting from an analysis of current practice, we isolate a set of desiderata for guiding the development of a parametrized benchmark selection algorithm. Our algorithm samples a benchmark set from a larger base set (or distribution) comprising a large variety of instances. This is done fully automatically, in a way that carefully calibrates instance hardness and instance similarity. We demonstrate the usefulness of this approach by means of empirical results showing that optimizing solvers on the benchmark sets produced by our method leads to better configurations than obtained based on the much larger, original sets.

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

Access this chapter

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 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

Institutional subscriptions

Notes

  1. 1.

    In ASP competitions, this deficit is counterbalanced by a modelling track, in which each participant can use its preferred modelling language.

  2. 2.

    http://www.satcompetition.org

  3. 3.

    Solution count ranking assesses solvers based on the number of solved instances.

  4. 4.

    Careful ranking compares pairs of solvers based on statistically significant performance differences and ranks solvers based on the resulting ranking graph.

  5. 5.

    http://asparagus.cs.uni-potsdam.de/

  6. 6.

    clasp won several first places in previous SAT, PB and ASP competitions.

References

  1. Balint, A., Belov, A., Järvisalo, M., Sinz, C.: Application and hard combinatorial benchmarks in SAT challenge. In: Proceedings of SAT Challenge 2012: Solver and Benchmark Descriptions. Department of CS Series of Publications B, vol. B-2012-2, pp. 69–71. University of Helsinki (2012)

    Google Scholar 

  2. Berre, D., Roussel, O., Simon, L.: http://www.satcompetition.org/2009/BenchmarksSelection.html (2009). Accessed 09 March 2012

  3. Van Gelder, A.: Careful ranking of multiple solvers with timeouts and ties. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 317–328. Springer, Heidelberg (2011)

    Google Scholar 

  4. Hoos, H., Stützle, T.: Stochastic Local Search: Foundations and Applications. Elsevier/Morgan Kaufmann, San Francisco (2004)

    Google Scholar 

  5. Sinz, C.: Visualizing SAT instances and runs of the DPLL algorithm. J. Autom. Reason. 39, 219–243 (2007)

    Article  MATH  Google Scholar 

  6. Nudelman, E., Leyton-Brown, K., Hoos, H., Devkar, A., Shoham, Y.: Understanding random SAT: beyond the clauses-to-variables ratio. In: Wallace, M. (ed.) CP 2004. LNCS, vol. 3258, pp. 438–452. Springer, Heidelberg (2004)

    Google Scholar 

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

    MATH  Google Scholar 

  8. Kadioglu, S., Malitsky, Y., Sabharwal, A., Samulowitz, H., Sellmann, M.: Algorithm selection and scheduling. In: Lee, J. (ed.) CP 2011. LNCS, vol. 6876, pp. 454–469. Springer, Heidelberg (2011)

    Google Scholar 

  9. 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)

    Google Scholar 

  10. Kadioglu, S., Malitsky, Y., Sellmann, M., Tierney, K.: ISAC - instance-specific algorithm configuration. In: Proceedings of ECAI’10, pp. 751–756. IOS Press (2010)

    Google Scholar 

  11. Brglez, F., Li, X., Stallmann, F.: The role of a skeptic agent in testing and benchmarking of sat algorithms (2002)

    Google Scholar 

  12. 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)

    Google Scholar 

  13. Gebser, M., Kaminski, R., Kaufmann, B., Schaub, T., Schneider, M.T., Ziller, S.: A portfolio solver for answer set programming: preliminary report. In: Delgrande, J.P., Faber, W. (eds.) LPNMR 2011. LNCS, vol. 6645, pp. 352–357. Springer, Heidelberg (2011)

    Google Scholar 

  14. O’Mahony, E., Hebrard, E., Holland, A., Nugent, C., O’Sullivan, B.: Using case-based reasoning in an algorithm portfolio for constraint solving. In: AICS’08 (2008)

    Google Scholar 

  15. Hamerly, G., Elkan, C.: Learning the k in k-means. In: Proceedings of NIPS’03. MIT Press (2003)

    Google Scholar 

  16. Hill, T., Lewicki, P.: Statistics: Methods and Applications. StatSoft, Tulsa (2005)

    Google Scholar 

  17. Bayless, S., Tompkins, D., Hoos, H.: Evaluating instance generators by configuration. Submitted for publication (2012)

    Google Scholar 

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

    MATH  Google Scholar 

  19. Gebser, M., Kaminski, R., Kaufmann, B., Ostrowski, M., Schaub, T., Schneider, M.: Potassco: the potsdam answer set solving collection. AI Commun. 24(2), 105–124 (2011)

    MathSciNet  Google Scholar 

  20. Audemard, G., Simon, L.: Glucose 2.1. in the SAT challenge 2012. In: Proceedings of SAT Challenge 2012: Solver and Benchmark Descriptions. Department of CS Series of Publications B, vol. B-2012-2, pp. 23–23. University of Helsinki (2012)

    Google Scholar 

  21. Yasumoto, T.: Sinn. In: Proceedings of SAT Challenge 2012: Solver and Benchmark Descriptions. Department of CS Series of Publications B, vol. B-2012-2, pp. 61–61. University of Helsinki (2012)

    Google Scholar 

  22. Biere, A.: Lingeling and friends entering the SAT challenge 2012. In: Proceedings of SAT Challenge 2012: Solver and Benchmark Descriptions. Department of CS Series of Publications B, vol. B-2012-2, pp. 33–34. University of Helsinki (2012)

    Google Scholar 

  23. Cai, S., Luo, C., Su, K.: CCASAT: solver description. In: Proceedings of SAT Challenge 2012: Solver and Benchmark Descriptions. Department of CS Series of Publications B, vol. B-2012-2, pp. 13–14. University of Helsinki (2012)

    Google Scholar 

  24. Giunchiglia, E., Lierler, Y., Maratea, M.: Answer set programming based on propositional satisfiability. J. Autom. Reason. 36(4), 345–377 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  25. Simons, P., Niemelä, I., Soininen, T.: Extending and implementing the stable model semantics. Artif. Intell. 138(1–2), 181–234 (2002)

    Article  MATH  Google Scholar 

  26. Syrjänen, T.: Lparse 1.0 user’s manual

    Google Scholar 

Download references

Acknowledgments.

B. Kaufmann, T. Schaub and M. Schneider were partially supported by DFG under grants SCHA 550/8-3 and SCHA 550/9-1. H. Hoos was supported by an NSERC Discovery Grant and by the GRAND NCE.

Author information

Authors and Affiliations

  1. Department of Computer Science, University of British Columbia, Vancouver, BC, Canada

    Holger H. Hoos

  2. Institute of Computer Science, University of Potsdam, Potsdam, Germany

    B. Kaufmann, T. Schaub & M. Schneider

Authors
  1. Holger H. Hoos
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. B. Kaufmann
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. T. Schaub
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. M. Schneider
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Holger H. Hoos .

Editor information

Editors and Affiliations

  1. Università Catania Dipto. Matematica e Informatica, Catania, Italy

    Giuseppe Nicosia

  2. Industrial & Systems Engineering, University of Florida, Gainesville, Florida, USA

    Panos Pardalos

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hoos, H.H., Kaufmann, B., Schaub, T., Schneider, M. (2013). Robust Benchmark Set Selection for Boolean Constraint Solvers. In: Nicosia, G., Pardalos, P. (eds) Learning and Intelligent Optimization. LION 2013. Lecture Notes in Computer Science(), vol 7997. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-44973-4_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-44973-4_16

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-44972-7

  • Online ISBN: 978-3-642-44973-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation