Search Results

Documents authored by Li, Chu-Min

Artifact
Software
DOI: 10.4230/artifacts.26928
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}
}
Artifact
Software
DOI: 10.4230/artifacts.25917
DA_kissat_MAB

Authors: Jinghu Liang, Sami Cherif, and Chu-Min Li

Abstract
Cite as

Jinghu Liang, Sami Cherif, Chu-Min Li. DA_kissat_MAB (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-25917,
   title = {{DA\underlinekissat\underlineMAB}}, 
   author = {Liang, Jinghu and Cherif, Sami and Li, Chu-Min},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:6a87ea34fdb8dfef213682f2d9dbfd0523d605e1;origin=https://github.com/JinghuLiang/Duration_Aware_kissat_MAB;visit=swh:1:snp:87ac8f74937a77042d5513b82a8be598e191d0bf;anchor=swh:1:rev:6cb1221a9de2d01602294c3c5cf4e12e269007fe}{\texttt{swh:1:dir:6a87ea34fdb8dfef213682f2d9dbfd0523d605e1}} (visited on 2026-07-13)},
   url = {https://github.com/JinghuLiang/Duration_Aware_kissat_MAB},
   doi = {10.4230/artifacts.25917},
}
Document
DOI: 10.4230/LIPIcs.CP.2026.39
Not All Restarts Are Equal: MAB-Learning at the Right Time Scale for SAT

Authors: Jinghu Liang, Sami Cherif, and Chu-Min Li

Published in: LIPIcs, Volume 379, 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)

Abstract
Multi-Armed Bandit (MAB) mechanisms have proven effective for adaptive heuristic switching in modern CDCL SAT solvers, with Kissat_MAB and its variants demonstrating strong performance in recent SAT Competitions. However, while strategies like the Luby series generate restarts with high duration variability, standard bandit models treat each restart as a homogeneous unit. This mismatch can bias credit assignment and lead to suboptimal exploration–exploitation trade-offs between short and long restarts. In this paper, we study MAB-based heuristic selection under variable-duration restart policies and propose a duration-aware modification to both bandit feedback and selection mechanisms. Our approach normalizes and conditions rewards on the restarts and adapts exploration and exploitation accordingly, thereby better aligning bandit updates with the solver’s restart dynamics.
Cite as

Jinghu Liang, Sami Cherif, and Chu-Min Li. Not All Restarts Are Equal: MAB-Learning at the Right Time Scale for SAT. In 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 379, pp. 39:1-39:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{liang_et_al:LIPIcs.CP.2026.39,
  author =	{Liang, Jinghu and Cherif, Sami and Li, Chu-Min},
  title =	{{Not All Restarts Are Equal: MAB-Learning at the Right Time Scale for SAT}},
  booktitle =	{32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)},
  pages =	{39:1--39:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-432-1},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{379},
  editor =	{Beldiceanu, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2026.39},
  URN =		{urn:nbn:de:0030-drops-266718},
  doi =		{10.4230/LIPIcs.CP.2026.39},
  annote =	{Keywords: Satisfiablity, Branching, Restart, Multi-Armed Bandit}
}
Document
DOI: 10.4230/LIPIcs.CP.2026.60
Enhanced Lower Bound Computation in Branch-and-Bound for MaxSAT

Authors: Jialu Zhang, Chu-Min Li, Sami Cherif, and Shuolin Li

Published in: LIPIcs, Volume 379, 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)

Abstract
Maximum Satisfiability (MaxSAT) is an optimization extension of the Satisfiability (SAT) problem. In Branch-and-Bound (BnB) MaxSAT solving, the quality of the lower bound estimation is critical for effective search space pruning. State-of-the-art BnB solvers typically estimate this bound by identifying disjoint inconsistent subformulas (cores) via Unit Propagation (UP). However, a limitation of this standard approach is that UP fails to detect cores that exhibit complex dependencies with already identified cores. In this paper, we propose a further lookahead algorithm that leverages pre-detected cores to uncover additional disjoint inconsistencies, thereby tightening the lower bound. Experimental results demonstrate that the proposed algorithm significantly tightens the lower bound, enabling the state of the art BnB solver MaxCDCL to solve more instances.
Cite as

Jialu Zhang, Chu-Min Li, Sami Cherif, and Shuolin Li. Enhanced Lower Bound Computation in Branch-and-Bound for MaxSAT. In 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 379, pp. 60:1-60:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{zhang_et_al:LIPIcs.CP.2026.60,
  author =	{Zhang, Jialu and Li, Chu-Min and Cherif, Sami and Li, Shuolin},
  title =	{{Enhanced Lower Bound Computation in Branch-and-Bound for MaxSAT}},
  booktitle =	{32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)},
  pages =	{60:1--60:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-432-1},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{379},
  editor =	{Beldiceanu, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2026.60},
  URN =		{urn:nbn:de:0030-drops-266935},
  doi =		{10.4230/LIPIcs.CP.2026.60},
  annote =	{Keywords: Maximum Satisfiability, Branch and Bound, Lower Bound}
}
Artifact
Software
DOI: 10.4230/artifacts.22455
ROADEF_SCHEDULING

Authors: Sami Cherif, Heythem Sattoutah, Chu-Min Li, Corinne Lucet, and Laure Brisoux-Devendeville

Abstract
Cite as

Sami Cherif, Heythem Sattoutah, Chu-Min Li, Corinne Lucet, Laure Brisoux-Devendeville. ROADEF_SCHEDULING (Software, Source Code,~Data,~Benchmark). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-22455,
   title = {{ROADEF\underlineSCHEDULING}}, 
   author = {Cherif, Sami and Sattoutah, Heythem and Li, Chu-Min and Lucet, Corinne and Brisoux-Devendeville, Laure},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:7083377094f69163d37d30b77d740c72c562139d;origin=https://github.com/satoutahhaithem/ROADEF_SCHEDULING;visit=swh:1:snp:c34fc60c52e7d5289f8e1c049ce6ba5e0adc48d2;anchor=swh:1:rev:92a1a45786ba37797dda7d78f7d02347f6f2a0a8}{\texttt{swh:1:dir:7083377094f69163d37d30b77d740c72c562139d}} (visited on 2024-11-28)},
   url = {https://github.com/satoutahhaithem/ROADEF_SCHEDULING},
   doi = {10.4230/artifacts.22455},
}
Document
Short Paper
DOI: 10.4230/LIPIcs.CP.2024.34
Minimizing Working-Group Conflicts in Conference Session Scheduling Through Maximum Satisfiability (Short Paper)

Authors: Sami Cherif, Heythem Sattoutah, Chu-Min Li, Corinne Lucet, and Laure Brisoux-Devendeville

Published in: LIPIcs, Volume 307, 30th International Conference on Principles and Practice of Constraint Programming (CP 2024)

Abstract
This paper explores the application of Maximum Satisfiability (Max-SAT) to the complex problem of conference session scheduling, with a particular focus on minimizing working-group conflicts within the context of the ROADEF conference, the largest French-speaking event aimed at bringing together researchers from various fields such as combinatorial optimization and operational research. A Max-SAT model is introduced then enhanced with new variables, and solved through state-of-the-art solvers. The results of applying our formulation to data from ROADEF demonstrate its ability to effectively compute session schedules, while enabling to reduce the number of conflicts and the maximum number of parallel sessions compared to the handmade solutions proposed by the organizing committees. These findings underscore the potential of Max-SAT as a valuable tool for optimizing conference scheduling processes, offering a systematic and efficient solution that ensures a smoother and more productive experience for attendees and organizers alike.
Cite as

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 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 34:1-34:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{cherif_et_al:LIPIcs.CP.2024.34,
  author =	{Cherif, Sami and Sattoutah, Heythem and Li, Chu-Min and Lucet, Corinne and Brisoux-Devendeville, Laure},
  title =	{{Minimizing Working-Group Conflicts in Conference Session Scheduling Through Maximum Satisfiability}},
  booktitle =	{30th International Conference on Principles and Practice of Constraint Programming (CP 2024)},
  pages =	{34:1--34:11},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-336-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{307},
  editor =	{Shaw, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2024.34},
  URN =		{urn:nbn:de:0030-drops-207190},
  doi =		{10.4230/LIPIcs.CP.2024.34},
  annote =	{Keywords: Maximum Satisfiability, Scheduling, Modeling}
}
Document
DOI: 10.4230/LIPIcs.SAT.2024.8
Enhancing MaxSAT Local Search via a Unified Soft Clause Weighting Scheme

Authors: Yi Chu, Chu-Min Li, Furong Ye, and Shaowei Cai

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract
Local search has been widely applied to solve the well-known (weighted) partial MaxSAT problem, significantly influencing many real-world applications. The main difficulty to overcome when designing a local search algorithm is that it can easily fall into local optima. Clause weighting is a beneficial technique that dynamically adjusts the landscape of search space to help the algorithm escape from local optima. Existing works tend to increase the weights of falsified clauses, and such strategies may result in an unpredictable landscape of search space during the optimization process. Therefore, in this paper, we propose a Unified Soft Clause Weighting Scheme called Unified-SW, which increases the weights of all soft clauses in feasible local optima, whether they are satisfied or not, while preserving the hierarchy among them. We implemented Unified-SW in a new local search solver called USW-LS. Experimental results demonstrate that USW-LS, outperforms the state-of-the-art local search solvers across benchmarks from anytime tracks of recent MaxSAT Evaluations. More promisingly, a hybrid solver combining USW-LS and TT-Open-WBO-Inc won all four categories in the anytime track of MaxSAT Evaluation 2023.
Cite as

Yi Chu, Chu-Min Li, Furong Ye, and Shaowei Cai. Enhancing MaxSAT Local Search via a Unified Soft Clause Weighting Scheme. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{chu_et_al:LIPIcs.SAT.2024.8,
  author =	{Chu, Yi and Li, Chu-Min and Ye, Furong and Cai, Shaowei},
  title =	{{Enhancing MaxSAT Local Search via a Unified Soft Clause Weighting Scheme}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.8},
  URN =		{urn:nbn:de:0030-drops-205301},
  doi =		{10.4230/LIPIcs.SAT.2024.8},
  annote =	{Keywords: Weighted Partial MaxSAT, Local Search Method, Weighting Scheme}
}
Document
DOI: 10.4230/LIPIcs.CP.2021.38
Combining Clause Learning and Branch and Bound for MaxSAT

Authors: Chu-Min Li, Zhenxing Xu, Jordi Coll, Felip Manyà, Djamal Habet, and Kun He

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

Abstract
Branch and Bound (BnB) is a powerful technique that has been successfully used to solve many combinatorial optimization problems. However, MaxSAT is a notorious exception because BnB MaxSAT solvers perform poorly on many instances encoding interesting real-world and academic optimization problems. This has formed a prevailing opinion in the community stating that BnB is not so useful for MaxSAT, except for random and some special crafted instances. In fact, there has been no advance allowing to significantly speed up BnB MaxSAT solvers in the past few years, as illustrated by the absence of BnB solvers in the annual MaxSAT Evaluation since 2017. Our work aims to change this situation and proposes a new BnB MaxSAT solver, called MaxCDCL, by combining clause learning and an efficient bounding procedure. The experimental results show that, contrary to the prevailing opinion, BnB can be competitive for MaxSAT. MaxCDCL is ranked among the top 5 solvers of the 15 solvers that participated in the 2020 MaxSAT Evaluation, solving a number of instances that other solvers cannot solve. Furthermore, MaxCDCL, when combined with the best existing solvers, solves the highest number of instances of the MaxSAT Evaluations.
Cite as

Chu-Min Li, Zhenxing Xu, Jordi Coll, Felip Manyà, Djamal Habet, and Kun He. Combining Clause Learning and Branch and Bound for MaxSAT. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 38:1-38:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{li_et_al:LIPIcs.CP.2021.38,
  author =	{Li, Chu-Min and Xu, Zhenxing and Coll, Jordi and Many\`{a}, Felip and Habet, Djamal and He, Kun},
  title =	{{Combining Clause Learning and Branch and Bound for MaxSAT}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{38:1--38:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.38},
  URN =		{urn:nbn:de:0030-drops-153291},
  doi =		{10.4230/LIPIcs.CP.2021.38},
  annote =	{Keywords: MaxSAT, Branch\&Bound, CDCL}
}
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