Document Open Access Logo

NLIPSat: Satisfiability-Based Nonlinear Integer Programming Encoding Toolkit (Tool Paper)

Authors Zhengling Yangli , Zhifei Zheng , Sami Cherif , Rui Sá Shibasaki , Chu-Min Li

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2026.43.pdf
  • Filesize: 2.05 MB
  • 13 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Constraint and logic programming
  • Mathematics of computing → Combinatorial optimization
Keywords
  • Maximum Satisfiability
  • Nonlinear Integer Programming
  • Encodings
  • Tool

Metrics

Abstract

While Maximum Satisfiability (MaxSAT) has been successfully applied to a wide range of combinatorial optimization problems, the encoding of Nonlinear Integer Programming (NLIP) with polynomial functions into MaxSAT has so far only been studied at a theoretical level. In this paper, we introduce NLIPSat, the first tool capable of encoding bounded polynomial NLIP instances directly into Maximum Satisfiability. Building upon recent MaxSAT formulations for polynomial NLIP proposed in [Zhifei Zheng et al., 2025], NLIPSat enables the encoding of polynomial nonlinear objective functions as weighted soft clauses and also supports the encoding of hard non-linear polynomial constraints within a polynomial setting. Extensive experiments on different benchmarks show that NLIPSat outperforms the state-of-the-art SMT solver Z3 by a wide margin.

Cite As Get BibTex

Zhengling Yangli, Zhifei Zheng, Sami Cherif, Rui Sá Shibasaki, and Chu-Min Li. NLIPSat: Satisfiability-Based Nonlinear Integer Programming Encoding Toolkit (Tool Paper). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 43:1-43:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.SAT.2026.43

Author Details

Zhengling Yangli
  • Yunnan University, China
Zhifei Zheng
  • Gaoling School of AI, Renmin University of China, Beijing, China
Sami Cherif
  • MIS UR 4290, Université de Picardie Jules Verne, Amiens, France
Rui Sá Shibasaki
  • MIS UR 4290, Université de Picardie Jules Verne, Amiens, France
Chu-Min Li
  • MIS UR 4290, Université de Picardie Jules Verne, Amiens, France

Funding

This work is partially supported by the project ANR-24-CE23-6126 (BforSAT) and the Chair ANR-19-CHIA-0013 (Massal'IA), co-funded by the French national research agency and the French electricity distribution network operator Enedis. It was also granted access to HPC resources of "Plateforme MatriCS" within University of Picardie Jules Verne, co-funded by the European Union with the European Regional Development Fund (FEDER) and the Hauts-De-France Regional Council.

Supplementary Materials

References

  1. Carlos Ansótegui and Felip Manyà. Mapping problems with finite-domain variables into problems with boolean variables. In SAT 2004 - The Seventh International Conference on Theory and Applications of Satisfiability Testing, 10-13 May 2004, Vancouver, BC, Canada, Online Proceedings, 2004. URL: http://www.satisfiability.org/SAT04/programme/53.pdf.
  2. Fahiem Bacchus, Matti Järvisalo, and Ruben Martins. Maximum satisfiability. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 929-991. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA201008.
  3. Tomáš Balyo, Nils Froleyks, Marijn JH Heule, Markus Iser, Matti Järvisalo, and Martin Suda. Proceedings of sat competition 2020: Solver and benchmark descriptions. Department of Computer Science Series of Publications B ; Report B-2020-1 ; B-2020-1, 2020. Google Scholar
  4. Tomás Balyo, Marijn J. H. Heule, and Matti Järvisalo. SAT competition 2016: Recent developments. In Satinder Singh and Shaul Markovitch, editors, Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence, February 4-9, 2017, San Francisco, California, USA, pages 5061-5063. AAAI Press, 2017. URL: https://doi.org/10.1609/AAAI.V31I1.10641.
  5. Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. cvc5: A versatile and industrial-strength SMT solver. In Dana Fisman and Grigore Rosu, editors, Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I, Lecture Notes in Computer Science, pages 415-442. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-99524-9_24.
  6. Clark Barrett, Aaron Stump, Cesare Tinelli, et al. The smt-lib standard: Version 2.0. In Proceedings of the 8th international workshop on satisfiability modulo theories (Edinburgh, UK), volume 13, page 14, 2010. Google Scholar
  7. Daniel Le Berre and Anne Parrain. The sat4j library, release 2.2. J. Satisf. Boolean Model. Comput., 7(2-3):59-6, 2010. URL: https://doi.org/10.3233/SAT190075.
  8. Cristina Borralleras, Daniel Larraz, Enric Rodríguez-Carbonell, Albert Oliveras, and Albert Rubio. Incomplete SMT techniques for solving non-linear formulas over the integers. ACM Trans. Comput. Log., 20(4):25:1-25:36, 2019. URL: https://doi.org/10.1145/3340923.
  9. Sami Cherif, Heythem Sattoutah, Chu-Min Li, Corinne Lucet, and Laure Brisoux Devendeville. Minimizing working-group conflicts in conference session scheduling through maximum satisfiability (short paper). In Paul Shaw, editor, 30th International Conference on Principles and Practice of Constraint Programming, CP 2024, Girona, Spain, September 2-6, 2024, volume 307 of LIPIcs, pages 34:1-34:11. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.CP.2024.34.
  10. Jessica Davies and Fahiem Bacchus. Solving MAXSAT by solving a sequence of simpler SAT instances. In Jimmy Ho-Man Lee, editor, Principles and Practice of Constraint Programming - CP 2011 - 17th International Conference, CP 2011, Perugia, Italy, September 12-16, 2011. Proceedings, volume 6876 of Lecture Notes in Computer Science, pages 225-239. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-23786-7_19.
  11. Leonardo Mendonça de Moura and Nikolaj S. Bjørner. Z3: an efficient SMT solver. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, volume 4963 of Lecture Notes in Computer Science, pages 337-340. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78800-3_24.
  12. Marco A. Duran and Ignacio E. Grossmann. An outer-approximation algorithm for a class of mixed-integer nonlinear programs. Math. Program., 39(3):337, 1987. URL: https://doi.org/10.1007/BF02592081.
  13. Niklas Eén and Niklas Sörensson. Translating pseudo-boolean constraints into SAT. J. Satisf. Boolean Model. Comput., 2(1-4):1-26, 2006. URL: https://doi.org/10.3233/SAT190014.
  14. Fabio Furini, Emiliano Traversi, Pietro Belotti, Antonio Frangioni, Ambros M. Gleixner, Nick Gould, Leo Liberti, Andrea Lodi, Ruth Misener, Hans D. Mittelmann, Nikolaos V. Sahinidis, Stefan Vigerske, and Angelika Wiegele. QPLIB: a library of quadratic programming instances. Math. Program. Comput., 11(2):237-265, 2019. URL: https://doi.org/10.1007/S12532-018-0147-4.
  15. João Guerra and Inês Lynce. Reasoning over biological networks using maximum satisfiability. In Michela Milano, editor, Principles and Practice of Constraint Programming - 18th International Conference, CP 2012, Québec City, QC, Canada, October 8-12, 2012. Proceedings, volume 7514 of Lecture Notes in Computer Science, pages 941-956. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-33558-7_67.
  16. Aarti Gupta, Malay K. Ganai, and Chao Wang. Sat-based verification methods and applications in hardware verification. In Marco Bernardo and Alessandro Cimatti, editors, Formal Methods for Hardware Verification, 6th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2006, Bertinoro, Italy, May 22-27, 2006, Advanced Lectures, volume 3965 of Lecture Notes in Computer Science, pages 108-143. Springer, 2006. URL: https://doi.org/10.1007/11757283_5.
  17. Alexey Ignatiev, António Morgado, and João Marques-Silva. Pysat: A python toolkit for prototyping with SAT oracles. In Olaf Beyersdorff and Christoph M. Wintersteiger, editors, 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, volume 10929 of Lecture Notes in Computer Science, pages 428-437. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94144-8_26.
  18. Alexey Ignatiev, António Morgado, and João Marques-Silva. RC2: an efficient maxsat solver. J. Satisf. Boolean Model. Comput., 11(1):53-64, 2019. URL: https://doi.org/10.3233/SAT190116.
  19. Robert G. Jeroslow. There cannot be any algorithm for integer programming with quadratic constraints. Oper. Res., 21(1):221-224, 1973. URL: https://doi.org/10.1287/OPRE.21.1.221.
  20. Fuqi Jia, Rui Han, Pei Huang, Minghao Liu, Feifei Ma, and Jian Zhang. Improving bit-blasting for nonlinear integer constraints. In René Just and Gordon Fraser, editors, Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2023, Seattle, WA, USA, July 17-21, 2023, pages 14-25. ACM, 2023. URL: https://doi.org/10.1145/3597926.3598034.
  21. Chu Min Li and Felip Manyà. Maxsat, hard and soft constraints. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 903-927. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA201007.
  22. Shuolin Li, Chu-Min Li, Jordi Coll, Djamal Habet, and Felip Manyà. Improving the lower bound in branch-and-bound algorithms for maxsat. In Toby Walsh, Julie Shah, and Zico Kolter, editors, AAAI-25, Sponsored by the Association for the Advancement of Artificial Intelligence, February 25 - March 4, 2025, Philadelphia, PA, USA, pages 11272-11281. AAAI Press, 2025. URL: https://doi.org/10.1609/AAAI.V39I11.33226.
  23. Jesús A. De Loera, Raymond Hemmecke, Matthias Köppe, and Robert Weismantel. Integer polynomial optimization in fixed dimension. Math. Oper. Res., 31(1):147-153, 2006. URL: https://doi.org/10.1287/MOOR.1050.0169.
  24. Harry M Markowitz. Portfolio selection: efficient diversification of investments. Yale university press, 2008. Google Scholar
  25. Panos M. Pardalos, Franz Rendl, and Henry Wolkowicz. The quadratic assignment problem: A survey and recent developments. In Panos M. Pardalos and Henry Wolkowicz, editors, Quadratic Assignment and Related Problems, Proceedings of a DIMACS Workshop, New Brunswick, New Jersey, USA, May 20-21, 1993, volume 16 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 1-42. DIMACS/AMS, 1993. URL: https://doi.org/10.1090/DIMACS/016/01.
  26. Tobias Philipp and Peter Steinke. PBLib - A library for encoding pseudo-boolean constraints into CNF. In Marijn Heule and Sean A. Weaver, editors, Theory and Applications of Satisfiability Testing - SAT 2015 - 18th International Conference, Austin, TX, USA, September 24-27, 2015, Proceedings, Lecture Notes in Computer Science, pages 9-16. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-24318-4_2.
  27. Zhengling Yangli, Zhifei Zheng, Sami Cherif, Rui Sá Shibasaki, and Chu-Min Li. NLIPSat. Software, (visited on 2026-06-29). URL: https://github.com/ZhenglingYangli/NLIPSat-Toolkit
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.26928
  28. Jialu Zhang, Chu Min Li, Sami Cherif, Shuolin Li, and Zhifei Zheng. Integer linear programming preprocessing for maximum satisfiability. In 37th IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2025, Athens, Greece, November 3-5, 2025, pages 408-414. IEEE, 2025. URL: https://doi.org/10.1109/ICTAI66417.2025.00061.
  29. Zhifei Zheng, Sami Cherif, and Rui Sá Shibasaki. Optimizing power peaks in simple assembly line balancing through maximum satisfiability. In 36th IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2024, Herndon, VA, USA, October 28-30, 2024, pages 363-370. IEEE, 2024. URL: https://doi.org/10.1109/ICTAI62512.2024.00060.
  30. Zhifei Zheng, Sami Cherif, Rui Sá Shibasaki, Chu Min Li, and Jialu Zhang. Exact approaches for the diverse satisfiability problem. In Giovanni Casini, Besik Dundua, and Temur Kutsia, editors, Logics in Artificial Intelligence - 19th European Conference, JELIA 2025, Kutaisi, Georgia, September 1-4, 2025, Proceedings, Part II, volume 16094 of Lecture Notes in Computer Science, pages 207-224. Springer, 2025. URL: https://doi.org/10.1007/978-3-032-04590-4_15.
  31. Zhifei Zheng, Sami Cherif, Rui Sá Shibasaki, Chu Min Li, and Jialu Zhang. Maximum satisfiability formulations for nonlinear integer programming. In Giovanni Casini, Besik Dundua, and Temur Kutsia, editors, Logics in Artificial Intelligence - 19th European Conference, JELIA 2025, Kutaisi, Georgia, September 1-4, 2025, Proceedings, Part II, volume 16094 of Lecture Notes in Computer Science, pages 190-206. Springer, 2025. URL: https://doi.org/10.1007/978-3-032-04590-4_14.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact