Skip to main content
SpringerLink
Log in

Solving MaxSAT by Successive Calls to a SAT Solver

  • Conference paper
  • First Online:
Proceedings of SAI Intelligent Systems Conference (IntelliSys) 2016 (IntelliSys 2016)

Part of the book series: Lecture Notes in Networks and Systems ((LNNS,volume 15))

Included in the following conference series:

Abstract

The Maximum Satisfiability (MaxSAT) is the problem of determining the maximum number of clauses of a given Boolean formula in Conjunctive Normal Form (CNF) that can be satisfied by an assignment of truth values to the variables of the formula. Many exact solvers for MaxSAT have been developed during recent years, and many of them were presented in the well-known SAT Conference. Algorithms for MaxSAT generally fall into two categories: (1) branch and bound algorithms and (2) algorithms that use successive calls to a SAT solver (SAT-based), which this paper in on. In practical problems, SAT-based algorithms have been shown to be more efficient. This paper provides an experimental investigation to compare the performance of recent SAT-based and branch and bound algorithms on benchmarks of the MaxSAT Evaluations.

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

References

  1. Ansótegui, C., Bonet, M.L., Levy, J.: Solving (weighted) partial maxsat through satisfiability testing. In: Theory and Applications of Satisfiability Testing-SAT 2009, pp. 427–440 (2009)

    Google Scholar 

  2. Ansótegui, C., Bonet, M.L., Gabàs, J., Levy, J.: Improving sat-based weighted maxSAT solvers. In: Principles and Practice of Constraint Programming, pp. 86–101. Springer (2012)

    Google Scholar 

  3. Ansótegui, C., Bonet, M.L., Gabàs, J., Levy, J.: Improving WPM2 for (weighted) partial maxSAT. In: Principles and Practice of Constraint Programming, pp. 117–132. Springer (2013)

    Google Scholar 

  4. Ansótegui, C., Bonet, M.L., Levy, J.: A New Algorithm for Weighted Partial maxSAT (2010)

    Google Scholar 

  5. Ansótegui, C., Bonet, M.L., Levy, J.: SAT-based maxSAT algorithms. Artif. Intell. 196, 77–105 (2013)

    Google Scholar 

  6. Ansótegui, C., Malitsky, Y., Sellmann, M.: MaxSAT by Improved Instance-Specific Algorithm Configuration (2014)

    Google Scholar 

  7. Davies, J., Bacchus, F.: Postponing optimization to speed up maxSAT solving. In: Principles and Practice of Constraint Programming, pp. 247–262. Springer (2013)

    Google Scholar 

  8. Eén, N., Sörensson, N.: Translating pseudo-Boolean constraints into SAT. JSAT 2(1–4), 1–26 (2006)

    MATH  Google Scholar 

  9. Fu, Z., Malik, S.: On solving the partial MAX-SAT problem. In: Theory and Applications of Satisfiability Testing-SAT 2006, pp. 252–265 (2006)

    Google Scholar 

  10. Gent, I.P.: Arc consistency in sat. In: ECAI, vol. 2, pp. 121–125 (2002)

    Google Scholar 

  11. Heras, F., Morgado, A., Marques-Silva, J.: Core-guided binary search algorithms for maximum satisfiability. In: Proceedings of the AAAI National Conference (AAAI) (2011)

    Google Scholar 

  12. Koshimura, M., Zhang, T., Fujita, H., Hasegawa, R.: QMaxSAT: a partial Max-SAT solver system description. J. Satisfiability Boolean Model. Comput. 8, 95–100 (2012)

    MathSciNet  MATH  Google Scholar 

  13. Le Berre, D., Parrain, A.: The SAT4J library, release 2.2 system description. J. Satisfiability Boolean Model. Comput. 7, 59–64 (2010)

    Google Scholar 

  14. Li, C.M., Manyà, F., Mohamedou, N., Planes, J.: Exploiting cycle structures in Max-SAT. In: Theory and Applications of Satisfiability Testing-SAT 2009, pp. 467–480 (2009)

    Google Scholar 

  15. Marques-Silva, J.: The MSUNCORE MaxSAT solver. In: SAT 2009 Competitive Events Booklet: Preliminary Version, p. 151 (2009)

    Google Scholar 

  16. Marques-Silva, J., Planes, J.: On Using Unsatisfiability for Solving Maximum Satisfiability. arXiv preprint arXiv:0712.1097 (2007)

  17. Marques-Silva, J., Planes, J.: Algorithms for maximum satisfiability using unsatisfiable cores. In: Proceedings of the Conference on Design, Automation and Test in Europe, pp. 408–413. ACM (2008)

    Google Scholar 

  18. 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  MATH  Google Scholar 

  19. Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Annual Design Automation Conference, pp. 530–535. ACM (2001)

    Google Scholar 

  20. Prestwich, S.: Variable dependency in local search: Prevention is better than cure. In: Theory and Applications of Satisfiability Testing-SAT 2007, pp. 107–120. Springer (2007)

    Google Scholar 

  21. Prestwich, S.D.: CNF encodings. In: Handbook of Satisfiability, vol. 185, pp. 75–97 (2009)

    Google Scholar 

  22. Sinz, C.: Towards an optimal CNF encoding of Boolean cardinalityconstraints. In: Principles and Practice of Constraint Programming-CP 2005, pp. 827–831 (2005)

    Google Scholar 

Download references

Acknowledgments

I would like to thank Dr. Hassan Aly (Department of Mathematics, Cairo University), Dr. Rasha Shaheen (Department of Mathematics, Cairo University) and Dr. Carlos Ansótegui (University of Lleida) for helping me throughout this research.

Author information

Authors and Affiliations

  1. Department of Mathematics, Faculty of Science, Cairo University, Giza, 12613, Egypt

    Mohamed El Halaby

Authors
  1. Mohamed El Halaby
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Mohamed El Halaby .

Editor information

Editors and Affiliations

  1. Faculty of Computing and Engineering, School of Computing and Mathematics, University of Ulster at Jordanstown, Newtownabbey, United Kingdom

    Yaxin Bi

  2. The Science and Information (SAI) Organization, Bradford, West Yorkshire, United Kingdom

    Supriya Kapoor

  3. The Science and Information (SAI) Organization, Bradford, West Yorkshire, United Kingdom

    Rahul Bhatia

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG

About this paper

Cite this paper

El Halaby, M. (2018). Solving MaxSAT by Successive Calls to a SAT Solver. In: Bi, Y., Kapoor, S., Bhatia, R. (eds) Proceedings of SAI Intelligent Systems Conference (IntelliSys) 2016. IntelliSys 2016. Lecture Notes in Networks and Systems, vol 15. Springer, Cham. https://doi.org/10.1007/978-3-319-56994-9_31

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-56994-9_31

  • Published:

  • Publisher Name: Springer, Cham

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

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

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics

Search

Navigation