Advertisement

Constraints

, Volume 24, Issue 2, pp 133–161 | Cite as

N-level Modulo-Based CNF encodings of Pseudo-Boolean constraints for MaxSAT

  • Aolong ZhaEmail author
  • Miyuki Koshimura
  • Hiroshi Fujita
Article

Abstract

Many combinatorial problems in various fields can be translated to Maximum Satisfiability (MaxSAT) problems. Although the general problem is \(\mathcal {N}\mathcal {P}\)-hard, more and more practical problems may be solved due to the significant effort which has been devoted to the development of efficient solvers. The art of constraints encoding is as important as the art of devising algorithms for MaxSAT. In this paper, we present several encoding methods of pseudo-Boolean constraints into Boolean satisfiability problems in Conjunctive Normal Form (CNF) formula, which are based on the idea of modular arithmetic and only generate auxiliary variables for each unique combination of weights. These techniques are efficient in encoding and solving MaxSAT problems. In particular, our solvers won the partial MaxSAT industrial category from 2010 through 2012 and ranked second in the 2017 main weighted track of the MaxSAT evaluation. We prove the correctness and the pseudo-polynomial space complexity of our encodings and also give a heuristics of the base selection for modular arithmetic. Our experimental results show that our encoding compactly encodes the constraints, and the obtained clauses are efficiently handled by a state-of-the-art SAT solver.

Keywords

MaxSAT Pseudo-Boolean constraints Encoding Modular arithmetic 

Notes

Acknowledgements

This work was supported by JSPS KAKENHI Grant Numbers JP16K00304, JP17K00307.

References

  1. 1.
    Aavani, A., Mitchell, D.G., Ternovska, E. (2013). New encoding for translating pseudo-boolean constraints into SAT. In Proceedings of the 10th symposium on abstraction, reformulation, and approximation, SARA 2013, 11-12 July 2013, Leavenworth, Washington, USA. AAAI Press. http://www.aaai.org/ocs/index.php/SARA/SARA13/paper/view/7212.
  2. 2.
    Abío, I., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E., Mayer-Eichberger, V. (2012). A new look at BDDs for Pseudo-Boolean constraints. Journal of Artificial Intelligence Research, 45(1), 443–480.  https://doi.org/10.1613/jair.3653.MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Aggoun, A., & Vazacopoulos, A. (2004). Solving sports scheduling and timetabling problems with constraint programming. In Butenko, S., Gil-Lafuente, J. & Pardalos, P.M. (Eds.) Economics, management and optimization in sports (pp. 243–264). Berlin: Springer.  https://doi.org/10.1007/978-3-540-24734-0_15.
  4. 4.
    Ansótegui, C., Bonet, M.L., Levy, J. (2009). Solving (weighted) partial MaxSAT through satisfiability testing. In Kullmann, O. (Ed.) Theory and applications of satisfiability testing - SAT 2009, 12th international conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009. Proceedings, Lecture Notes in Computer Science (Vol. 5584, pp. 427–440). Berlin: Springer.  https://doi.org/10.1007/978-3-642-02777-2_39.
  5. 5.
    Ansótegui, C., Bonet, M.L., Levy, J. (2010). A new algorithm for weighted partial MaxSAT. In Proceedings of the 24th AAAI conference on artificial intelligence, AAAI 2010, Atlanta, Georgia, USA, July 11-15, 2010. AAAI Press. http://www.aaai.org/ocs/index.php/AAAI/AAAI10/paper/view/1774.
  6. 6.
    AnsóTegui, C., Bonet, M. L., Levy, J. (2013). SAT-Based maxSAT algorithms. Artificial Intelligence, 196, 77–105.  https://doi.org/10.1016/j.artint.2013.01.002.MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Asín, R., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E. (2011). Cardinality networks: a theoretical and empirical study. Constraints, 16(2), 195–221.  https://doi.org/10.1007/s10601-010-9105-0.MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Audemard, G., Lagniez, J., Simon, L. (2013). Improving glucose for incremental SAT solving with assumptions: application to MUS extraction. In Järvisalo, M., & Gelder, A.V. (Eds.) Theory and applications of satisfiability testing - SAT 2013 - 16th international conference, Helsinki, Finland, July 8-12, 2013. Proceedings, Lecture Notes in Computer Science (Vol. 7962, pp. 309–317). Berlin: Springer.  https://doi.org/10.1007/978-3-642-39071-5_23.
  9. 9.
    Audemard, G., & Simon, L. (2009). Predicting learnt clauses quality in modern SAT solvers. In IJCAI 2009, Proceedings of the 21st international joint conference on artificial intelligence, Pasadena, California, USA, July 11-17, 2009 (pp. 399–404). Morgan Kaufmann Publishers Inc. http://ijcai.org/Proceedings/09/Papers/074.pdf.
  10. 10.
    Bailleux, O., & Boufkhad, Y. (2003). Efficient CNF encoding of Boolean cardinality constraints. In Rossi, F. (Ed.) Principles and practice of constraint programming - CP 2003, 9th international conference, CP 2003, Kinsale, Ireland, September 29 - October 3, 2003, Proceedings, Lecture Notes in Computer Science (Vol. 2833, pp. 108–122). Berlin: Springer.  https://doi.org/10.1007/978-3-540-45193-8_8.
  11. 11.
    Bailleux, O., Boufkhad, Y., Roussel, O. (2006). A translation of Pseudo Boolean constraints to SAT. JSAT, 2(1-4), 191–200. https://satassociation.org/jsat/index.php/jsat/article/view/25.zbMATHGoogle Scholar
  12. 12.
    Bailleux, O., Boufkhad, Y., Roussel, O. (2009). New encodings of Pseudo-Boolean constraints into CNF. In Kullmann, O. (Ed.) Theory and applications of satisfiability testing - SAT 2009, 12th international conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009. Proceedings, Lecture Notes in Computer Science (Vol. 5584, pp. 181–194). Berlin: Springer.  https://doi.org/10.1007/978-3-642-02777-2_19.
  13. 13.
    Berre, D.L., & Parrain, A. (2010). The Sat4j library, release 2.2. JSAT, 7(2-3), 59–6. https://satassociation.org/jsat/index.php/jsat/article/view/82.Google Scholar
  14. 14.
    Codish, M., Fekete, Y., Fuhs, C., Schneider-Kamp, P. (2011). Optimal base encodings for Pseudo-Boolean constraints. In Abdulla, P.A., & Leino, K.R.M. (Eds.) Tools and algorithms for the construction and analysis of systems - 17th international conference, TACAS 2011, held as part of the joint European conferences on theory and practice of software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings, Lecture Notes in Computer Science (Vol. 6605, pp. 189–204). Berlin: Springer.  https://doi.org/10.1007/978-3-642-19835-9_16.
  15. 15.
    Codish, M., & Zazon-Ivry, M. (2010). Pairwise cardinality networks. In Clarke, E.M., & Voronkov, A. (Eds.) Logic for programming, artificial intelligence, and reasoning - 16th international conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers, Lecture Notes in Computer Science (Vol. 6355, pp. 154–172). Berlin: Springer.  https://doi.org/10.1007/978-3-642-17511-4_10.
  16. 16.
    Cook, S.A. (1971). The complexity of theorem-proving procedures. In Proceedings of the 3rd annual ACM symposium on theory of computing, STOC ’71 (pp. 151–158). ACM.  https://doi.org/10.1145/800157.805047.
  17. 17.
    Davies, J., & Bacchus, F. (2011). Solving MAXSAT by solving a sequence of simpler SAT instances. In Lee, J. (Ed.) Principles and practice of constraint programming - CP 2011 - 17th international conference, CP 2011, Perugia, Italy, September 12-16, 2011. Proceedings, Lecture Notes in Computer Science (Vol. 6876, pp. 225–239). Berlin: Springer.  https://doi.org/10.1007/978-3-642-23786-7_19.
  18. 18.
    Davies, J., & Bacchus, F. (2013). Exploiting the power of mip solvers in maxsat. In Järvisalo, M., & Gelder, A.V. (Eds.) Theory and applications of satisfiability testing - SAT 2013 - 16th international conference, Helsinki, Finland, July 8-12, 2013. Proceedings, Lecture Notes in Computer Science (Vol. 7962, pp. 166–181). Berlin: Springer.  https://doi.org/10.1007/978-3-642-39071-5_13.
  19. 19.
    Davies, J., & Bacchus, F. (2013). Postponing optimization to speed up MAXSAT solving. In Schulte, C. (Ed.) Principles and practice of constraint programming - 19th international conference, CP 2013, Uppsala, Sweden, September 16-20, 2013. Proceedings, Lecture Notes in Computer Science (Vol. 8124, pp. 247–262). Berlin: Springer.  https://doi.org/10.1007/978-3-642-40627-0_21.
  20. 20.
    Eén, N., & Sörensson, N. (2006). Translating Pseudo-Boolean constraints into SAT. JSAT, 2(1-4), 1–26. https://satassociation.org/jsat/index.php/jsat/article/view/18.zbMATHGoogle Scholar
  21. 21.
    Fei, L., Mize, L., Moon, C., Mullen, B., Singhal, S. (2010). Constraint analysis and debugging for multi-million instance SoC designs. In 11th international symposium on quality electronic design (ISQED), 22-24 March 2010, San Jose, CA, USA (pp. 422–427): IEEE.  https://doi.org/10.1109/ISQED.2010.5450540.
  22. 22.
    Fekete, Y., & Codish, M. (2014). Simplifying Pseudo-Boolean constraints in residual number systems. In Sinz, C., & Egly, U. (Eds.) Theory and applications of satisfiability testing - SAT 2014 - 17th international conference, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, Lecture Notes in Computer Science (Vol. 8561, pp. 351–366). Springer International Publishing.  https://doi.org/10.1007/978-3-319-09284-3_26.
  23. 23.
    Fu, Z., & Malik, S. (2006). On solving the partial MAX-SAT problem. In Biere, A., & Gomes, C.P. (Eds.) Theory and applications of satisfiability testing - SAT 2006, 9th international conference, Seattle, WA, USA, August 12-15, 2006, Proceedings, Lecture Notes in Computer Science (Vol. 4121, pp. 252–265). Berlin: Springer.  https://doi.org/10.1007/11814948_25.
  24. 24.
    Gent, I.P. (2002). Arc consistency in SAT. In Proceedings of the 15th Eureopean conference on artificial intelligence, ECAI’2002, Lyon, France, July 2002 (pp. 121–125): IOS Press. https://ipg.host.cs.st-andrews.ac.uk/papers/ipgECAI.ps.
  25. 25.
    Hayata, S., & Hasegawa, R. (2015). Improvement in CNF encoding of cardinality constraints for weighted partial MaxSAT. SIG-FPAI, in Japanese, B4(4), 85–90. http://id.nii.ac.jp/1004/00000592.Google Scholar
  26. 26.
    Heras, F., Morgado, A., Marques-Silva, J. (2011). Core-guided binary search algorithms for maximum satisfiability. In Proceedings of the 25th AAAI conference on artificial intelligence, AAAI 2011, San Francisco, California, USA, August 7-11, 2011: AAAI Press. http://www.aaai.org/ocs/index.php/AAAI/AAAI11/paper/view/3713.
  27. 27.
    Heyer, L.J. (2008). A mathematical optimization problem in bioinformatics. PRIMUS, 18(1), 101–118.  https://doi.org/10.1080/10511970701744992.CrossRefGoogle Scholar
  28. 28.
    Hölldobler, S., Manthey, N., Steinke, P. (2012). A compact encoding of pseudo-boolean constraints into SAT. In Glimm, B., & Krüger, A. (Eds.) KI 2012: Advances in artificial intelligence - 35th annual German conference on AI, Saarbrücken, Germany, September 24-27, 2012. Proceedings, Lecture Notes in Computer Science (Vol. 7526, pp. 107–118). Berlin: Springer.  https://doi.org/10.1007/978-3-642-33347-7_10.
  29. 29.
    Hooker, J.N. (2007). Planning and scheduling by Logic-Based benders decomposition. Operations Research, 55(3), 588–602.  https://doi.org/10.1287/opre.1060.0371.MathSciNetCrossRefzbMATHGoogle Scholar
  30. 30.
    Ignatiev, A., Morgado, A., Marques-Silva, J. (2018). PySAT: a python toolkit for prototyping with SAT Oracles. In Beyersdorff, O., & Wintersteiger, C.M. (Eds.) Theory and applications of satisfiability testing - SAT 2018 - 21st international conference, SAT 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, Lecture Notes in Computer Science (Vol. 10929, pp. 428–437). Berlin: Springer.  https://doi.org/10.1007/978-3-319-94144-8_26.
  31. 31.
    Joshi, S., Martins, R., Manquinho, V.M. (2015). Generalized totalizer encoding for pseudo-boolean constraints. In Pesant, G. (Ed.) Principles and practice of constraint programming - 21st international conference, CP 2015, Cork, Ireland, August 31 - September 4, 2015, Proceedings, Lecture Notes in Computer Science (Vol. 9255, pp. 200–209). Springer International Publishing.  https://doi.org/10.1007/978-3-319-23219-5_15.
  32. 32.
    Kellerer, H., Pferschy, U., Pisinger, D. (2004). Knapsack problems. Berlin: Springer.  https://doi.org/10.1007/978-3-540-24777-7.CrossRefzbMATHGoogle Scholar
  33. 33.
    Koshimura, M., Zhang, T., Fujita, H., Hasegawa, R. (2012). QMaxSAT: a partial Max-SAT solver. JSAT, 8(1/2), 95–100. https://satassociation.org/jsat/index.php/jsat/article/view/98.MathSciNetzbMATHGoogle Scholar
  34. 34.
    Larrosa, J., & Schiex, T. (2004). Solving weighted CSP by maintaining arc consistency. Artificial Intelligence, 159(1), 1–26.  https://doi.org/10.1016/j.artint.2004.05.004.MathSciNetCrossRefzbMATHGoogle Scholar
  35. 35.
    Li, C.M., & Manyà, F. (2009). MaxSAT, hard and soft constraints. In Biere, A., Heule, M., van Maaren, H., Walsh, T. (Eds.) Handbook of satisfiability. Frontiers in Artificial Intelligence and Applications, (Vol. 185, pp. 613–631). Amsterdam: IOS Press.  https://doi.org/10.3233/978-1-58603-929-5-613.
  36. 36.
    Manquinho, V.M., Silva, J.P.M., Planes, J. (2009). Algorithms for weighted boolean optimization. In Kullmann, O. (Ed.) Theory and applications of satisfiability testing - SAT 2009, 12th international conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009. Proceedings, Lecture Notes in Computer Science (Vol. 5584, pp. 495–508). Berlin: Springer.  https://doi.org/10.1007/978-3-642-02777-2_45.
  37. 37.
    Manthey, N., Philipp, T., Steinke, P. (2014). A more compact translation of pseudo-boolean constraints into CNF such that generalized arc consistency is maintained. In Lutz, C., & Thielscher, M. (Eds.) KI 2014: advances in artificial intelligence - 37th annual German conference on AI, Stuttgart, Germany, September 22-26, 2014. Proceedings, Lecture Notes in Computer Science (Vol. 8736, pp. 123–134). Springer International Publishing.  https://doi.org/10.1007/978-3-319-11206-0_13.
  38. 38.
    Ogawa, T., Liu, Y., Hasegawa, R., Koshimura, M., Fujita, H. (2013). Modulo based CNF encoding of cardinality constraints and its application to MaxSAT solvers. In 2013 IEEE 25th international conference on tools with artificial intelligence, Herndon, VA, USA, November 4-6, 2013 (pp. 9–17): IEEE Computer Society.  https://doi.org/10.1109/ICTAI.2013.13.
  39. 39.
    Paxian, T., Reimer, S., Becker, B. (2018). Dynamic polynomial watchdog encoding for solving weighted MaxSAT. In Beyersdorff, O., & Wintersteiger, C.M. (Eds.) Theory and applications of satisfiability testing - SAT 2018 - 21st international conference, SAT 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, Lecture Notes in Computer Science (Vol. 10929, pp. 37–53). Berlin: Springer.  https://doi.org/10.1007/978-3-319-94144-8_3.
  40. 40.
    Roussel, O., & Manquinho, V.M. (2004). Pseudo-Boolean and cardinality constraints. In Biere, A., Heule, M., van Maaren, H., Walsh, T. (Eds.) Handbook of satisfiability. Frontiers in Artificial Intelligence and Applications (Vol. 185, pp. 695–733). Amsterdam: IOS Press.  https://doi.org/10.3233/978-1-58603-929-5-695.
  41. 41.
    Silva, J.P.M., & Lynce, I. (2007). Towards robust CNF encodings of cardinality constraints. In Bessière, C. (Ed.) Principles and practice of constraint programming - CP 2007, 13th international conference, CP 2007, Providence, RI, USA, September 23-27, 2007, Proceedings, Lecture Notes in Computer Science (Vol. 4741, pp. 483–497). Berlin: Springer.  https://doi.org/10.1007/978-3-540-74970-7_35.
  42. 42.
    Silva, J.P.M., Lynce, I., Malik, S. (2009). Conflict-driven clause learning SAT solvers. In Biere, A., Heule, M., van Maaren, H., Walsh, T. (Eds.) Handbook of satisfiability. Frontiers in Artificial Intelligence and Applications (Vol. 185, pp. 131–153). Amsterdam: IOS Press.  https://doi.org/10.3233/978-1-58603-929-5-131.
  43. 43.
    Sinz, C. (2005). Towards an optimal CNF encoding of Boolean cardinality constraints. In van Beek, P. (Ed.) Principles and practice of constraint programming - CP 2005, 11th international conference, CP 2005, Sitges, Spain, October 1-5, 2005, Proceedings, Lecture Notes in Computer Science (Vol. 3709, pp. 827–831). Berlin: Springer.  https://doi.org/10.1007/11564751_73.
  44. 44.
    Warners, J.P. (1998). A linear-time transformation of linear inequalities into conjunctive normal form. Information Processing Letters, 68(2), 63–69.  https://doi.org/10.1016/S0020-0190(98)00144-6.MathSciNetCrossRefzbMATHGoogle Scholar
  45. 45.
    Wood, R.G., & Rutenbar, R.A. (1997). FPGA routing and routability estimation via Boolean satisfiability. In Proceedings of the 1997 ACM 5th international symposium on field-programmable gate arrays, FPGA ’97 (pp. 119–125). ACM.  https://doi.org/10.1145/258305.258322.
  46. 46.
    Zha, A., Koshimura, M., Fujita, H. (2017). A hybrid encoding of pseudo-boolean constraints into CNF. In Conference on technologies and applications of artificial intelligence, TAAI 2017, Taipei, Taiwan, December 1-3, 2017 (pp. 9–12). IEEE Computer Society.  https://doi.org/10.1109/TAAI.2017.15.
  47. 47.
    Zha, A., Nomoto, K., Ueda, S., Koshimura, M., Sakurai, Y., Yokoo, M. (2017). Coalition structure generation for partition function games utilizing a concise graphical representation. In An, B., Bazzan, A., Leite, J., Villata, S., van der Torre, L. (Eds.) PRIMA 2017: principles and practice of multi-agent systems - 20th international conference, Nice, France, October 30 - November 3, 2017, Proceedings, Lecture Notes in Computer Science (Vol. 10621, pp. 143–159): Springer International Publishing.  https://doi.org/10.1007/978-3-319-69131-2_9.
  48. 48.
    Zha, A., Uemura, N., Koshimura, M., Fujita, H. (2017). Mixed radix weight totalizer encoding for Pseudo-Boolean constraints. In 2017 IEEE 29th international conference on tools with artificial intelligence, Boston, MA, USA, November 6-8, 2017 (pp. 868–875). IEEE Computer Society.  https://doi.org/10.1109/ICTAI.2017.00135.

Copyright information

© Springer Science+Business Media, LLC, part of Springer Nature 2019

Authors and Affiliations

  1. 1.Kyushu UniversityFukuokaJapan

Personalised recommendations