DROPS

Artifact

Software

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

Search Results

Documents authored by Liang, Jinghu

DA_kissat_MAB

Abstract

Cite as

Not All Restarts Are Equal: MAB-Learning at the Right Time Scale for SAT

Abstract

Cite as

Thanks for your feedback!

Could not send message