Open-WBO: A Modular MaxSAT Solver, | SpringerLink
Skip to main content
Springer Nature Link
Log in

Open-WBO: A Modular MaxSAT Solver,

  • Conference paper
Theory and Applications of Satisfiability Testing – SAT 2014 (SAT 2014)

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

Abstract

This paper presents open-wbo, a new MaxSAT solver. open-wbo has two main features. First, it is an open-source solver that can be easily modified and extended. Most MaxSAT solvers are not available in open-source, making it hard to extend and improve current MaxSAT algorithms. Second, open-wbo may use any MiniSAT-like solver as the underlying SAT solver. As many other MaxSAT solvers, open-wbo relies on successive calls to a SAT solver. Even though new techniques are proposed for SAT solvers every year, for many MaxSAT solvers it is hard to change the underlying SAT solver. With open-wbo, advances in SAT technology will result in a free improvement in the performance of the solver. In addition, the paper uses open-wbo to evaluate the impact of using different SAT solvers in the performance of MaxSAT algorithms.

Supported by the ERC project 280053.

Partially supported by FCT grants ASPEN (PTDC/EIA-CCO/110921/2009), POLARIS (PTDC/EIA-CCO/123051/2010), and INESC-ID’s multiannual PIDDAC funding PEst-OE/EEI/LA0021/2011.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Achá, R.A., Nieuwenhuis, R.: Curriculum-based course timetabling with SAT and MaxSAT. Annals of Operations Research, 1–21 (2012)

    Google Scholar 

  2. Ansótegui, C., Bonet, M.L., Gabàs, J., Levy, J.: Improving SAT-Based Weighted MaxSAT Solvers. In: Milano, M. (ed.) CP 2012. LNCS, vol. 7514, pp. 86–101. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  3. Ansótegui, C., Bonet, M.L., Levy, J.: Solving (Weighted) Partial MaxSAT through Satisfiability Testing. In: Kullmann [18], pp. 427–440

    Google Scholar 

  4. Ansótegui, C., Manyà, F.: Mapping Problems with Finite-Domain Variables into Problems with Boolean Variables. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 1–15. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  5. Asín, R., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E.: Practical algorithms for unsatisfiability proof and core generation in SAT solvers. AI Communications 23(2-3), 145–157 (2010)

    MATH  MathSciNet  Google Scholar 

  6. Asín, R., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E.: Cardinality Networks: a theoretical and empirical study. Constraints 16(2), 195–221 (2011)

    Article  MATH  MathSciNet  Google Scholar 

  7. Audemard, G., Lagniez, J.M., Simon, L.: Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 309–317. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  8. Audemard, G., Simon, L.: Predicting Learnt Clauses Quality in Modern SAT Solvers. In: Boutilier, C. (ed.) International Joint Conference on Artificial Intelligence, pp. 399–404 (2009)

    Google Scholar 

  9. Audemard, G., Simon, L.: Glucose 2.3 in the SAT 2013 Competition. In: Proceedings of SAT Competition 2013: Solver and Benchmark Descriptions [10], pp. 42–43

    Google Scholar 

  10. Balint, A., Belov, A., Heule, M., Järvisalo, M.: Proceedings of SAT Competition 2013: Solver and Benchmark Descriptions. Tech. rep., Department of Computer Science Series of Publications B, vol. B-2013-1, University of Helsinki, Helsinki (2013)

    Google Scholar 

  11. Chen, J.: Solvers with a Bit-Encoding Phase Selection Policy and a Decision-Depth-Sensitive Restart Policy. In: Proceedings of SAT Competition 2013: Solver and Benchmark Descriptions [10], pp. 44–45

    Google Scholar 

  12. Eén, N., Sörensson, N.: An Extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  13. Fu, Z., Malik, S.: On Solving the Partial MAX-SAT Problem. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 252–265. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  14. Gent, I.P., Nightingale, P.: A new encoding of All Different into SAT. In: International Workshop on Modelling and Reformulating Constraint Satisfaction Problems (2004)

    Google Scholar 

  15. Hölldobler, S., Manthey, N., Steinke, P.: A Compact Encoding of Pseudo-Boolean Constraints into SAT. In: Glimm, B., Krüger, A. (eds.) KI 2012. LNCS, vol. 7526, pp. 107–118. Springer, Heidelberg (2012)

    Google Scholar 

  16. Janota, M., Lynce, I., Manquinho, V., Marques-Silva, J.: PackUp: Tools for Package Upgradability Solving. Journal on Satisfiability, Boolean Modeling and Computation 8(1/2), 89–94 (2012)

    MathSciNet  Google Scholar 

  17. Koshimura, M., Zhang, T., Fujita, H., Hasegawa, R.: QMaxSAT: A Partial Max-SAT Solver. Journal on Satisfiability, Boolean Modeling and Computation 8, 95–100 (2012)

    MathSciNet  Google Scholar 

  18. Kullmann, O. (ed.): SAT 2009. LNCS, vol. 5584. Springer, Heidelberg (2009)

    MATH  Google Scholar 

  19. Le Berre, D., Parrain, A.: The Sat4j library, release 2.2. Journal on Satisfiability, Boolean Modeling and Computation 7(2-3), 59–66 (2010)

    Google Scholar 

  20. Le Berre, D., Rapicault, P.: Dependency Management for the Eclipse Ecosystem: Eclipse P2, Metadata and Resolution. In: International Workshop on Open Component Ecosystems, pp. 21–30. ACM (2009)

    Google Scholar 

  21. Li, C.M., Manyà, F.: MaxSAT, Hard and Soft Constraints. In: Handbook of Satisfiability, pp. 613–631. IOS Press (2009)

    Google Scholar 

  22. Luby, M., Sinclair, A., Zuckerman, D.: Optimal Speedup of Las Vegas Algorithms. Information Processing Letters 47(4), 173–180 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  23. Manquinho, V., Marques-Silva, J., Planes, J.: Algorithms for Weighted Boolean Optimization. In: Kullmann [18], pp. 495–508

    Google Scholar 

  24. Marques-Silva, J., Argelich, J., Graça, A., Lynce, I.: Boolean lexicographic optimization: algorithms & applications. Annals of Mathematics and Artificial Intelligence 62(3-4), 317–343 (2011)

    Article  MATH  MathSciNet  Google Scholar 

  25. Martins, R., Manquinho, V.M., Lynce, I.: On Partitioning for Maximum Satisfiability. In: Raedt, L.D., Bessière, C., Dubois, D., Doherty, P., Frasconi, P., Heintz, F., Lucas, P.J.F. (eds.) European Conference on Artificial Intelligence. Frontiers in Artificial Intelligence and Applications, vol. 242, pp. 913–914. IOS Press (2012)

    Google Scholar 

  26. Morgado, A., Heras, F., Liffiton, M., Planes, J., Marques-Silva, J.: Iterative and core-guided MaxSAT solving: A survey and assessment. Constraints 18(4), 478–534 (2013)

    Article  MathSciNet  Google Scholar 

  27. Nabeshima, H., Iwanuma, K., Inoue, K.: GLUEMINISAT2.2.7. In: Proceedings of SAT Competition 2013: Solver and Benchmark Descriptions [10], pp. 46–47

    Google Scholar 

  28. Ogawa, T., Liu, Y., Hasegawa, R., Koshimura, M., Fujita, H.: Modulo Based CNF Encoding of Cardinality Constraints and Its Application to MaxSAT Solvers. In: International Conference on Tools with Artificial Intelligence, pp. 9–17. IEEE (2013)

    Google Scholar 

  29. Oh, C.: gluH: Modified Version of glucose 2.1. In: Proceedings of SAT Competition 2013: Solver and Benchmark Descriptions [10], p. 48

    Google Scholar 

  30. Pipatsrisawat, K., Darwiche, A.: A Lightweight Component Caching Scheme for Satisfiability Solvers. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 294–299. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  31. Wieringa, S.: GlucoRed. In: Proceedings of SAT Competition 2013: Solver and Benchmark Descriptions [10], pp. 40–41

    Google Scholar 

  32. Yasumoto, T., Okugawa, T.: SINNminisat. In: Proceedings of SAT Competition 2013 : Solver and Benchmark Descriptions [10], p. 85

    Google Scholar 

  33. Yasumoto, T., Okugawa, T.: ZENN. In: Proceedings of SAT Competition 2013: Solver and Benchmark Descriptions [10], p. 95

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Oxford, United Kingdom

    Ruben Martins

  2. INESC-ID / Instituto Superior Técnico, Universidade de Lisboa, Portugal

    Vasco Manquinho & Inês Lynce

Authors
  1. Ruben Martins
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Vasco Manquinho
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Inês Lynce
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Karlsruher Institut für Technologie (KIT), Am Fasanengarten 5, 76131, Karlsruhe, Germany

    Carsten Sinz

  2. TU Wien, Favoritenstraße 9-11, 1040, Wien, Austria

    Uwe Egly

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Martins, R., Manquinho, V., Lynce, I. (2014). Open-WBO: A Modular MaxSAT Solver, . In: Sinz, C., Egly, U. (eds) Theory and Applications of Satisfiability Testing – SAT 2014. SAT 2014. Lecture Notes in Computer Science, vol 8561. Springer, Cham. https://doi.org/10.1007/978-3-319-09284-3_33

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-09284-3_33

  • Publisher Name: Springer, Cham

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

  • Online ISBN: 978-3-319-09284-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation