DROPS

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

Search Results

Documents authored by Li, Shuolin

Enhanced Lower Bound Computation in Branch-and-Bound for MaxSAT

Abstract

Cite as

Thanks for your feedback!

Could not send message