2026-07-20T05:58:30Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:26349 2026-07-16T10:50:13Z ddc:004 open_access

NLIPSat: Satisfiability-Based Nonlinear Integer Programming Encoding Toolkit (Tool Paper) Yangli, Zhengling Zheng, Zhifei Cherif, Sami Shibasaki, Rui Sá Li, Chu-Min Maximum Satisfiability Nonlinear Integer Programming Encodings Tool 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Zhengling Yangli and Zhifei Zheng and Sami Cherif and Rui Sá Shibasaki and Chu-Min Li 2026 Is Part Of LIPIcs, Volume 377, 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2026.43 urn:nbn:de:0030-drops-263492 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.43 eng https://creativecommons.org/licenses/by/4.0/legalcode