DROPS

Document

DOI: 10.4230/LIPIcs.SAT.2026.21

PALSAT: Deep Cooperation of Unit Propagation and Local Search in Incomplete SAT Solving

Authors: Mingming Jin, Zhijie Kuang, Jiongzhi Zheng, Kun Mao, and Kun He

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

Abstract

The Boolean Satisfiability (SAT) problem is a fundamental NP-complete problem. Algorithms for SAT include complete ones, typically based on Conflict-Driven Clause Learning (CDCL) methods, and incomplete ones, mostly following local search frameworks. CDCL solvers perform very well on complex structured instances. Local search (LS) algorithms cannot compete with CDCL solvers on structured instances, but show good performance on random and crafted instances, and also serve as an important component in top CDCL solvers. This raises a natural question: can techniques from complete SAT solving be used to improve incomplete solvers? This paper proposes the PALSAT (Progressive Activation Local Search for SAT) incomplete solver to answer it, which integrates the core techniques from both sides, Unit Propagation (UP) and LS. PALSAT starts from a subproblem, which relaxes many variables, and uses UP to progressively activate the search space (i.e., expand the subproblem). When a conflict is encountered, LS is invoked to repair it by searching all variables induced in the subproblem and the conflict. PALSAT ensures that the subproblem size increases monotonically and that the search process gradually approaches the full formula. In PALSAT, UP can guide growth direction based on the structure, and LS can efficiently repair conflicts. Their cooperation leads to some promising results. After a decade of evolution in CCAnr and probSAT variants, PALSAT represents a new incomplete algorithm framework with significantly better performance across various benchmarks.

Cite as

Mingming Jin, Zhijie Kuang, Jiongzhi Zheng, Kun Mao, and Kun He. PALSAT: Deep Cooperation of Unit Propagation and Local Search in Incomplete SAT Solving. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 21:1-21:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{jin_et_al:LIPIcs.SAT.2026.21,
  author =	{Jin, Mingming and Kuang, Zhijie and Zheng, Jiongzhi and Mao, Kun and He, Kun},
  title =	{{PALSAT: Deep Cooperation of Unit Propagation and Local Search in Incomplete SAT Solving}},
  booktitle =	{29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
  pages =	{21:1--21:18},
  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.21},
  URN =		{urn:nbn:de:0030-drops-263277},
  doi =		{10.4230/LIPIcs.SAT.2026.21},
  annote =	{Keywords: Satisfiability Problem, Local Search Algorithm, Unit Propagation, Subproblem Expansion}
}

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

Document

DOI: 10.4230/LIPIcs.ITCS.2021.25

Dynamic Inference in Probabilistic Graphical Models

Authors: Weiming Feng, Kun He, Xiaoming Sun, and Yitong Yin

Published in: LIPIcs, Volume 185, 12th Innovations in Theoretical Computer Science Conference (ITCS 2021)

Abstract

Probabilistic graphical models, such as Markov random fields (MRFs), are useful for describing high-dimensional distributions in terms of local dependence structures. The {probabilistic inference} is a fundamental problem related to graphical models, and sampling is a main approach for the problem. In this paper, we study probabilistic inference problems when the graphical model itself is changing dynamically with time. Such dynamic inference problems arise naturally in today’s application, e.g. multivariate time-series data analysis and practical learning procedures. We give a dynamic algorithm for sampling-based probabilistic inferences in MRFs, where each dynamic update can change the underlying graph and all parameters of the MRF simultaneously, as long as the total amount of changes is bounded. More precisely, suppose that the MRF has n variables and polylogarithmic-bounded maximum degree, and N(n) independent samples are sufficient for the inference for a polynomial function N(⋅). Our algorithm dynamically maintains an answer to the inference problem using Õ(n N(n)) space cost, and Õ(N(n) + n) incremental time cost upon each update to the MRF, as long as the Dobrushin-Shlosman condition is satisfied by the MRFs. This well-known condition has long been used for guaranteeing the efficiency of Markov chain Monte Carlo (MCMC) sampling in the traditional static setting. Compared to the static case, which requires Ω(n N(n)) time cost for redrawing all N(n) samples whenever the MRF changes, our dynamic algorithm gives a 𝛺^~(min{n, N(n)})-factor speedup. Our approach relies on a novel dynamic sampling technique, which transforms local Markov chains (a.k.a. single-site dynamics) to dynamic sampling algorithms, and an "algorithmic Lipschitz" condition that we establish for sampling from graphical models, namely, when the MRF changes by a small difference, samples can be modified to reflect the new distribution, with cost proportional to the difference on MRF.

Cite as

Weiming Feng, Kun He, Xiaoming Sun, and Yitong Yin. Dynamic Inference in Probabilistic Graphical Models. In 12th Innovations in Theoretical Computer Science Conference (ITCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 185, pp. 25:1-25:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{feng_et_al:LIPIcs.ITCS.2021.25,
  author =	{Feng, Weiming and He, Kun and Sun, Xiaoming and Yin, Yitong},
  title =	{{Dynamic Inference in Probabilistic Graphical Models}},
  booktitle =	{12th Innovations in Theoretical Computer Science Conference (ITCS 2021)},
  pages =	{25:1--25:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-177-1},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{185},
  editor =	{Lee, James R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2021.25},
  URN =		{urn:nbn:de:0030-drops-135643},
  doi =		{10.4230/LIPIcs.ITCS.2021.25},
  annote =	{Keywords: Dynamic inference, probabilistic graphical model, Gibbs sampling, Markov random filed}
}

Search Results

Documents authored by He, Kun

PALSAT: Deep Cooperation of Unit Propagation and Local Search in Incomplete SAT Solving

Abstract

Cite as

Combining Clause Learning and Branch and Bound for MaxSAT

Abstract

Cite as

Dynamic Inference in Probabilistic Graphical Models

Abstract

Cite as

Thanks for your feedback!

Could not send message