DiverSAT: A Novel and Effective Local Search Algorithm for Diverse SAT Problem
Jiaxin Liang, Junping Zhou, Minghao Yin
Abstract
For many real-world problems, users are often interested not only in finding a single solution but in obtaining a sufficiently diverse collection of solutions. In this work, we consider the Diverse SAT problem, aiming to find a set of diverse satisfying assignments for a given propositional formula. We propose a novel and effective local search algorithm, DiverSAT, to solve the problem. To cope with diversity, we introduce three heuristics and a perturbation strategy based on some relevant information. We conduct extensive experiments on a large number of public benchmarks, collected from semiformal hardware verification, logistics planning, and other domains. The results show that DiverSAT outperforms the existing algorithms on most of these benchmarks.
BibTeX
@article{Liang_Zhou_Yin_2025, title={DiverSAT: A Novel and Effective Local Search Algorithm for Diverse SAT Problem}, volume={39}, url={https://ojs.aaai.org/index.php/AAAI/article/view/33228}, DOI={10.1609/aaai.v39i11.33228}, abstractNote={For many real-world problems, users are often interested not only in finding a single solution but in obtaining a sufficiently diverse collection of solutions. In this work, we consider the Diverse SAT problem, aiming to find a set of diverse satisfying assignments for a given propositional formula. We propose a novel and effective local search algorithm, DiverSAT, to solve the problem. To cope with diversity, we introduce three heuristics and a perturbation strategy based on some relevant information. We conduct extensive experiments on a large number of public benchmarks, collected from semiformal hardware verification, logistics planning, and other domains. The results show that DiverSAT outperforms the existing algorithms on most of these benchmarks.}, number={11}, journal={Proceedings of the AAAI Conference on Artificial Intelligence}, author={Liang, Jiaxin and Zhou, Junping and Yin, Minghao}, year={2025}, month={Apr.}, pages={11290-11298} }