Skip to main content
Log in

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

  • Published:
Constraints Aims and scope Submit manuscript

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.

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

Access this article

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
Fig. 4

Similar content being viewed by others

Notes

  1. https://sites.google.com/site/qmaxsat

  2. Kyushu University is called “Kyushu Daigaku” or “Q-dai” in Japanese.

  3. http://www.maxsat.udl.cat

  4. If a clause only contains a single literal, then it is called a unit clause.

  5. “Unweighted” means that all the Boolean variables take a weight of 1.

  6. http://www.maxhs.org

  7. http://mse17.cs.helsinki.fi

  8. http://pysathq.github.io

  9. https://maxsat-evaluations.github.io/2018/

References

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  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.

    Article  MathSciNet  MATH  Google Scholar 

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

    MATH  Google Scholar 

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

    MATH  Google Scholar 

  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. 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. 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. 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. 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. 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. Heyer, L.J. (2008). A mathematical optimization problem in bioinformatics. PRIMUS, 18(1), 101–118. https://doi.org/10.1080/10511970701744992.

    Article  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  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. 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. Kellerer, H., Pferschy, U., Pisinger, D. (2004). Knapsack problems. Berlin: Springer. https://doi.org/10.1007/978-3-540-24777-7.

    Book  MATH  Google Scholar 

  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.

    MathSciNet  MATH  Google Scholar 

  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.

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

Download references

Acknowledgements

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

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Aolong Zha.

Additional information

Publisher’s note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Zha, A., Koshimura, M. & Fujita, H. N-level Modulo-Based CNF encodings of Pseudo-Boolean constraints for MaxSAT. Constraints 24, 133–161 (2019). https://doi.org/10.1007/s10601-018-9299-0

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10601-018-9299-0

Keywords

Navigation