DROPS

Artifact

Software

NLIPSat

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

Abstract

Cite as

Zhengling Yangli, Zhifei Zheng, Sami Cherif, Rui Sá Shibasaki, Chu-Min Li. NLIPSat (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-26928,
   title = {{NLIPSat}}, 
   author = {Yangli, Zhengling and Zheng, Zhifei and Cherif, Sami and Shibasaki, Rui S\'{a} and Li, Chu-Min},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:1567209c46a147ae48868eca1e8a5b44f4fceed3;origin=https://github.com/ZhenglingYangli/NLIPSat-Toolkit;visit=swh:1:snp:ab40e9a04170812cbc1e7545f1e7cd0bfa88a38a;anchor=swh:1:rev:95f138d8b5721c72011108a89f865bc6c342e254}{\texttt{swh:1:dir:1567209c46a147ae48868eca1e8a5b44f4fceed3}} (visited on 2026-07-16)},
   url = {https://github.com/ZhenglingYangli/NLIPSat-Toolkit},
   doi = {10.4230/artifacts.26928},
}

Document

Tool Paper

DOI: 10.4230/LIPIcs.SAT.2026.43

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

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

Published in: LIPIcs, Volume 377, 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)

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

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)

Copy BibTex To Clipboard

@InProceedings{yangli_et_al:LIPIcs.SAT.2026.43,
  author =	{Yangli, Zhengling and Zheng, Zhifei and Cherif, Sami and Shibasaki, Rui S\'{a} and Li, Chu-Min},
  title =	{{NLIPSat: Satisfiability-Based Nonlinear Integer Programming Encoding Toolkit}},
  booktitle =	{29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
  pages =	{43:1--43:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-431-4},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{377},
  editor =	{Ignatiev, Alexey and Szeider, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.43},
  URN =		{urn:nbn:de:0030-drops-263492},
  doi =		{10.4230/LIPIcs.SAT.2026.43},
  annote =	{Keywords: Maximum Satisfiability, Nonlinear Integer Programming, Encodings, Tool}
}

Search Results

Documents authored by Yangli, Zhengling

NLIPSat

Abstract

Cite as

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

Abstract

Cite as

Thanks for your feedback!

Could not send message