Skip to main content
SpringerLink
Log in

Exploiting subproblem optimization in SAT-based MaxSAT algorithms

  • Published:
Journal of Heuristics Aims and scope Submit manuscript

Abstract

The Maximum Satisfiability (MaxSAT) problem is an optimization variant of the Satisfiability (SAT) problem. Several combinatorial optimization problems can be translated into a MaxSAT formula. Among exact MaxSAT algorithms, SAT-based MaxSAT algorithms are the best performing approaches for real-world problems. We have extended the WPM2 algorithm by adding several improvements. In particular, we show that by solving some subproblems of the original MaxSAT instance we can dramatically increase the efficiency of WPM2. This led WPM2 to achieve the best overall results at the international MaxSAT Evaluation 2013 (MSE13) on industrial instances. Then, we present additional techniques and heuristics to further exploit the information retrieved from the resolution of the subproblems. We exhaustively analyze the impact of each improvement what contributes to our understanding of why they work. This architecture allows to convert exact algorithms into efficient incomplete algorithms. The resulting solver had the best results on industrial instances at the incomplete track of the latest international MSE.

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

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3

Similar content being viewed by others

Notes

  1. For the sake of clarity, we will obviate in the following mentioning the hardened soft clauses (\(H'\)) due to the clause hardening technique (see Sect. 4.2).

  2. There are only 66 industrial and 48 crafted instances for which was not found.

References

  • Andres, B., Kaufmann, B., Matheis, O., Schaub, T.: Unsatisfiability-based optimization in clasp. In: ICLP (Technical Communications), pp. 211–221 (2012)

  • Ansotegui, C.: Maxsat Latest Developments. Invited Tutorial at CP 2013 (2013a)

  • Ansotegui, C.: Tutorial: Maxsat Latest Developments (2013b)

  • Ansótegui, C., Gabàs, J.: Solving (weighted) partial maxsat with ilp. In: CPAIOR, pp. 403–409 (2013)

  • Ansótegui, C., Bonet, M.L., Levy, J.: On solving MaxSAT through SAT. In: Proceedings of the 12th International Conference of the Catalan Association for Artificial Intelligence (CCIA’09), pp. 284–292 (2009)

  • Ansotegui, C., Bonet, M.L., Levy, J.: Solving (weighted) partial maxsat through satisfiability testing. In: Proceedings of the 12th International Conference on Theory and Applications of Satisfiability Testing (SAT’09), pp. 427–440 (2009)

  • Ansotegui, C., Bonet, M.L., Levy, J.: A new algorithm for weighted partial maxsat. In: Proceedings the 24th National Conference on Artificial Intelligence (AAAI’10), pp. 867–872 (2010)

  • Ansótegui, C., Bofill, M., Palahí, M., Suy, J., Villaret, M.: A proposal for solving weighted CSPs with SMT. In: Proceedings of the 10th International Workshop on Constraint Modelling and Reformulation (ModRef 2011), pp. 5–19 (2011)

  • Ansótegui, C., Bonet, M.L., Gabàs, J., Levy, J.: Improving sat-based weighted maxsat solvers. In: Proceedings of the 18th International Conference on Principles and Practice of Constraint Programming (CP’12), pp. 86–101 (2012)

  • Ansótegui, C., Bonet, M.L., Gabàs, J., Levy, J.: Improving wpm2 for (weighted) partial maxsat. In: CP, pp. 117–132 (2013a)

  • Ansótegui, C., Bonet, M.L., Levy, J.: Sat-based maxsat algorithms. Artif. Intell. 196, 77–105 (2013b)

    Article  MATH  Google Scholar 

  • Argelich, J., Li, C.M., Manyà, F., Planes, J.: Maxsat evaluation. http://www.maxsat.udl.cat (2006–2014)

  • Bailleux, O., Boufkhad, Y., Roussel, O.: New encodings of pseudo-boolean constraints into cnf. In: SAT, pp. 181–194 (2009)

  • Barrett, C., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). http://www.SMT-LIB.org (2010)

  • Berre, D.L.: Sat4j, a satisfiability library for java. www.sat4j.org (2006)

  • Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009)

    Google Scholar 

  • Bofill, M., Palahí, M., Suy, J., Villaret, M.: Boosting weighted csp resolution with shared bdds. Proceedings of the 12th International Workshop on Constraint Modelling and Reformulation (ModRef 2013), pp. 57–73. Uppsala, Sweden (2013)

    Google Scholar 

  • Bonet, M.L., Levy, J., Manyà, F.: A complete calculus for Max-SAT. In: SAT, pp. 240–251 (2006)

  • Borchers, B., Furman, J.: A two-phase exact algorithm for max-sat and weighted max-sat problems. J. Comb. Optim. 2(4), 299–306 (1998)

    Article  MathSciNet  Google Scholar 

  • Cimatti, A., Franzén, A., Griggio, A., Sebastiani, R., Stenico, C.: Satisfiability modulo the theory of costs: foundations and applications. In: TACAS, pp. 99–113 (2010)

  • Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3rd edn. MIT Press, Cambridge, MA (2009)

    MATH  Google Scholar 

  • Davies, J., Bacchus, F.: Solving maxsat by solving a sequence of simpler sat instances. In: Proceedings of the 17th International Conference on Principles and Practice of Constraint Programming (CP’11), pp. 225–239 (2011)

  • Davies, J., Bacchus, F.: Exploiting the power of mip solvers in maxsat. In: SAT, pp. 166–181 (2013)

  • Dutertre, B., de Moura, L.: The Yices SMT Solver. http://yices.csl.sri.com (2014)

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

    MATH  Google Scholar 

  • Fu, Z., Malik, S.: On solving the partial max-sat problem. In: Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing (SAT’06), pp. 252–265 (2006)

  • Heras, F., Larrosa, J., Oliveras, A.: MiniMaxSat: A new weighted Max-SAT solver. In: Proceedings of the 10th International Conference on Theory and Applications of Satisfiability Testing (SAT’07), pp. 41–55 (2007)

  • Heras, F., Larrosa, J., Oliveras, A.: Minimaxsat: an efficient weighted max-sat solver. J. Artif. Intell. Res. (JAIR) 31, 1–32 (2008)

    MathSciNet  MATH  Google Scholar 

  • Heras, F., Morgado, A., Marques-Silva, J.: Core-guided binary search algorithms for maximum satisfiability. In: Proceedings of the 25th National Conference on Artificial Intelligence (AAAI’11), pp. 36–41 (2011)

  • Honjyo, K., Tanjo, T.: Shinmaxsat. A Weighted Partial Max-SAT Solver Inspired by MiniSat+. Information Science and Technology Center, Kobe University, Kobe (2012)

    Google Scholar 

  • Koshimura, M., Zhang, T., Fujita, H., Hasegawa, R.: Qmaxsat: a partial max-sat solver. JSAT 8(1/2), 95–100 (2012)

    MathSciNet  Google Scholar 

  • Kügel, A.: Improved exact solver for the weighted MAX-SAT problem. In: POS-10. Pragmatics of SAT, Edinburgh, UK, July 10, 2010, pp. 15–27 (2010)

  • Larrosa, J., Heras, F.: Resolution in max-sat and its relation to local consistency in weighted csps. In: IJCAI, pp. 193–198 (2005)

  • Larrosa, J., Heras, F., de Givry, S.: A logical approach to efficient max-sat solving. Artif. Intell. 172(2–3), 204–233 (2008)

    Article  MATH  Google Scholar 

  • Li, C.M., Manyà, F.: Maxsat, hard and soft constraints. In: Biere, A., van Maaren, H., Walsh, H. (eds.) Handbook of Satisfiability. IOS Press, Amsterdam (2009)

    Google Scholar 

  • Li, C.M., Manyà, F., Planes, J.: Detecting disjoint inconsistent subformulas for computing lower bounds for max-sat. In: AAAI, pp.86–91 (2006)

  • Li, C.M., Manyà, F., Planes, J.: New inference rules for Max-SAT. J. Artif. Intell. Res. (JAIR) 30, 321–359 (2007)

    Google Scholar 

  • Li, C.M., Manyà, F., Mohamedou, N.O., Planes, J.: Exploiting cycle structures in Max-SAT. In: Proceedings of the 12th International Conference on Theory and Applications of Satisfiability Testing (SAT’09), pp. 467–480 (2009)

  • Lin, H., Su, K.: Exploiting inference rules to compute lower bounds for Max-SAT solving. In: IJCAI’07, pp. 2334–2339 (2007)

  • Lin, H., Su, K., Li, C.M.: Within-problem learning for efficient lower bound computation in Max-SAT solving. In: Proceedings of the 23th National Conference on Artificial Intelligence (AAAI’08), pp. 351–356 (2008)

  • Manquinho, V., Marques-Silva, J., Planes, J.: Algorithms for weighted boolean optimization. In: Proceedings of the 12th International Conference on Theory and Applications of Satisfiability Testing (SAT’09), p.p 495–508 (2009)

  • Manquinho, V.M., Martins, R., Lynce, I.: Improving unsatisfiability-based algorithms for boolean optimization. In: Proceedings of the 13th International Conference on Theory and Applications of Satisfiability Testing (SAT’10), Lecture Notes in Computer Science, vol. 6175, pp. 181–193. Springer, (2010)

  • Marques-Silva, J., Argelich, J., Graça, A., Lynce, I.: Boolean lexicographic optimization: algorithms and applications. Ann. Math. Artif. Intell. 62(3–4), 317–343 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  • Martins, R., Manquinho, V.M., Lynce, I.: Exploiting cardinality encodings in parallel maximum satisfiability. In: ICTAI, pp. 313–320 (2011)

  • Martins, R., Manquinho, V.M., Lynce, I.: Clause sharing in parallel maxsat. In: LION, pp. 455–460 (2012)

  • Martins, R., Joshi, S., Manquinho, V.M., Lynce, I.: ncremental cardinality constraints for maxsat. In: Principles and Practice of Constraint Programming—20th International Conference, CP 2014, Lyon, France, September 8–12, 2014. Proceedings, pp. 531–548 (2014)

  • Morgado, A., Heras, F., Marques-Silva, J.: Improvements to core-guided binary search for maxsat. In: Proceedings of the 15th International Conference on Theory and Applications of Satisfiability Testing (SAT’12), pp. 284–297 (2012)

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

    Article  MathSciNet  Google Scholar 

  • Morgado, A., Heras, F., Marques-Silva, J.: Model-guided approaches for maxsat solving. In: 2013 IEEE 25th International Conference on Tools with Artificial Intelligence, Herndon, VA, USA, November 4–6, 2013, pp. 931–938 (2013b)

  • Morgado, A., Dodaro, C., Marques-Silva, J.: Core-guided maxsat with soft cardinality constraints. In: Proceedings of the Principles and Practice of Constraint Programming—20th International Conference, CP 2014, Lyon, France, September 8–12, 2014. pp. 564–573 (2014)

  • Narodytska, N., Bacchus, F.: Maximum satisfiability using core-guided maxsat resolution. In: Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, July 27–31, 2014, pp. 2717–2723. Québec City, Canada. (2014)

  • Nieuwenhuis, R., Oliveras, A.: On sat modulo theories and optimization problems. In: SAT, pp. 156–169 (2006)

  • Pipatsrisawat, K., Darwiche, A.: Clone: Solving weighted Max-SAT in a reduced search space. In: Australian Conference on Artificial Intelligence, pp. 223–233 (2007)

  • Raz, R.: Resolution lower bounds for the weak pigeonhole principle. In: Proceedings of the 17th Annual IEEE Conference on Computational Complexity, Montréal, Canada, May 21–24, 2002, p 3 (2002)

  • Razborov, A.A.: Improved resolution lower bounds for the weak pigeonhole principle. Electron. Colloquium Comput. Complex. (ECCC) 8(55), (2001)

  • Rossi, F., van Beek, P., Walsh, T. (eds.): Handbook of Constraint Programming. Elsevier, Amsterdam (2006)

    MATH  Google Scholar 

  • Sebastiani, R.: Lazy satisfiability modulo theories. J. Satisf. Boolean Model. Comput. 3(3–4), 141–224 (2007)

    MathSciNet  MATH  Google Scholar 

  • Sörensen, K.: Metaheuristics the metaphor exposed. Int. Trans. Oper. Res. 22(1), 3–18 (2015). doi:10.1111/itor.12001

    Article  MathSciNet  Google Scholar 

Download references

Acknowledgments

Research partially supported by the Ministerio de Economía y Competividad research project TASSAT2: TIN2013-48031-C4-4-P and Google Faculty Research Award program.

Author information

Authors and Affiliations

  1. DIEI, Universitat de Lleida, Lleida, Spain

    Carlos Ansótegui & Joel Gabàs

  2. IIIA-CSIC, Barcelona, Spain

    Jordi Levy

Authors
  1. Carlos Ansótegui
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Joel Gabàs
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jordi Levy
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Carlos Ansótegui.

Appendix

Appendix

See Tables 11, 12, 13, 14, 15 and 16.

Table 11 Impact of WPM2 improvements, compared on the industrial instances of MSE13 (number and mean ratio of solved instances)
Full size table
Table 12 Impact of WPM2 improvements, compared on the crafted instances of MSE13 (number and mean ratio of solved instances)
Full size table
Table 13 \(wpm2_{shucgo}\) compared to MSE13 best complete solvers on the industrial instances of MSE13 (number and mean ratio of solved instances)
Full size table
Table 14 \(wpm2_{shucgo}\) compared to MSE13 best complete solvers on the crafted instances of MSE13 (number and mean ratio of solved instances)
Full size table
Table 15 \(wpm2_{shucgo}\) incomplete compared to MSE13 incomplete solvers on the industrial instances of MSE13 (number and mean ratio of solved instances)
Full size table
Table 16 \(wpm2_{shucgo}\) incomplete compared to MSE13 incomplete solvers on the crafted instances of MSE13 (number and mean ratio of solved instances)
Full size table

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Ansótegui, C., Gabàs, J. & Levy, J. Exploiting subproblem optimization in SAT-based MaxSAT algorithms. J Heuristics 22, 1–53 (2016). https://doi.org/10.1007/s10732-015-9300-7

Download citation

  • Received:

  • Revised:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10732-015-9300-7

Keywords

Search

Navigation