Skip to main content
SpringerLink
Log in

SpyBug: Automated Bug Detection in the Configuration Space of SAT Solvers

  • Conference paper
  • First Online:
Theory and Applications of Satisfiability Testing – SAT 2016 (SAT 2016)

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

Abstract

Automated configuration is used to improve the performance of a SAT solver. Increasing the space of possible parameter configurations leverages the power of configuration but also leads to harder maintainable code and to more undiscovered bugs. We present the tool SpyBug that finds erroneous minimal parameter configurations of SAT solvers and their parameter specification to help developers to identify and narrow down bugs in their solvers. The importance of SpyBug is shown by the bugs we found for four well-known SAT solvers that won prices in international competitions.

N. Manthey—Supported by the DFG grant HO 1294/11-1.

M. Lindauer—Supported by the DFG under Emmy Noether grant HU 1900/2-1.

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.

    Such a collection could be generated with fuzzing tools [7].

  2. 2.

    http://www.cs.ubc.ca/labs/beta/Projects/SMAC/v2.08.00/manual.pdf.

  3. 3.

    When reproducing the buggy configuration with the native binary, the parameters that might be added to the solver call in the wrapper script must be considered.

References

  1. Artho, C., Biere, A., Seidl, M.: Model-based testing for verification back-ends. In: Veanes, M., Viganò, L. (eds.) TAP 2013. LNCS, vol. 7942, pp. 39–55. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  2. Balint, A., Manthey, N.: SparrowToRiss. In: Belov et al. [3], pp. 77–78

    Google Scholar 

  3. Belov, A., Diepold, D., Heule, M., Järvisalo, M. (eds.): Proceedings of SAT Competition 2014: Solver and Benchmark Descriptions, Department of Computer Science Series of Publications B, vol. B-2014-2. University of Helsinki (2014)

    Google Scholar 

  4. Biere, A.: Lingeling, plingeling and treengeling entering the sat competition 2013. In: Proceedings of SAT Competition 2013, pp. 51–52 (2013)

    Google Scholar 

  5. Biere, A.: Yet another local search solver and Lingeling and friends entering the SAT competition. In: Belov et al. [3], pp. 39–40 (2014)

    Google Scholar 

  6. Biere, A., Cimatti, A., Claessen, K.L., Jussila, T., McMillan, K., Somenzi, F.: Benchmarks from the 2008 hardware model checking competition (HWMCC 2008) (2008). http://fmv.jku.at/hwmcc08/benchmarks.html

  7. Brummayer, R., Lonsing, F., Biere, A.: Automated testing and debugging of SAT and QBF solvers. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 44–57. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  8. Falkner, S., Lindauer, M., Hutter, F.: SpySMAC: automated configuration and performance analysis of SAT solvers. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 215–222. Springer, Heidelberg (2015). doi:10.1007/978-3-319-24318-4_16

    Chapter  Google Scholar 

  9. Gebser, M., Kaufmann, B., Schaub, T.: Conflict-driven answer set solving: from theory to practice. Artif. Intell. 187–188, 52–89 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  10. Hutter, F., Hoos, H.H., Leyton-Brown, K.: Automated configuration of mixed integer programming solvers. In: Lodi, A., Milano, M., Toth, P. (eds.) CPAIOR 2010. LNCS, vol. 6140, pp. 186–202. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

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

    MATH  Google Scholar 

  13. Hutter, F., Lindauer, M., Balint, A., Bayless, S., Hoos, H.H., Leyton-Brown, K.: The configurable SAT solver challenge. CoRR (2015). http://arxiv.org/abs/1505.01221

  14. Järvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 355–370. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  15. Manthey, N.: Riss 4.27. In: Belov et al. [3], pp. 65–67

    Google Scholar 

  16. Maric, F.: Formal verification of a modern SAT solver by shallow embedding into isabelle/hol. Theor. Comput. Sci. 411(50), 4333–4356 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  17. Oe, D., Stump, A., Oliver, C., Clancy, K.: versat: a verified modern SAT solver. In: Kuncak, V., Rybalchenko, A. (eds.) Verification, Model Checking, and Abstract Interpretation. LNCS, vol. 7148, pp. 363–378. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  18. Oh, C.: MiniSat HACK 999ED, MiniSat HACK 1430ED and SWDiA5BY. In: Belov et al.[3], p. 46

    Google Scholar 

  19. Roussel, O.: Controlling a solver execution with the runsolver tool. J. Satisfiability Boolean Model. Comput. 7(4), 139–144 (2011)

    MathSciNet  MATH  Google Scholar 

  20. Silva, V., Kroening, D., Weissenbacher, G.: A survey of automated techniques for formal software verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 27(7), 1165–1178 (2008)

    Article  Google Scholar 

  21. Soos, M.: CryptoMiniSat v4. In: Belov et al. [3], p. 23

    Google Scholar 

  22. Zarpas, E.: Benchmarking SAT solvers for bounded model checking. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 340–354. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Technische Universität Dresden, Dresden, Germany

    Norbert Manthey

  2. University of Freiburg, Freiburg, Germany

    Marius Lindauer

Authors
  1. Norbert Manthey
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Marius Lindauer
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Marius Lindauer .

Editor information

Editors and Affiliations

  1. Aix-Marseille Université, Marseille, France

    Nadia Creignou

  2. Université d'Artois, Lens, France

    Daniel Le Berre

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Manthey, N., Lindauer, M. (2016). SpyBug: Automated Bug Detection in the Configuration Space of SAT Solvers. In: Creignou, N., Le Berre, D. (eds) Theory and Applications of Satisfiability Testing – SAT 2016. SAT 2016. Lecture Notes in Computer Science(), vol 9710. Springer, Cham. https://doi.org/10.1007/978-3-319-40970-2_36

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-40970-2_36

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-40969-6

  • Online ISBN: 978-3-319-40970-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation