DiverSAT: A Novel and Effective Local Search Algorithm for Diverse SAT Problem
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.
Cite
Text
Liang et al. "DiverSAT: A Novel and Effective Local Search Algorithm for Diverse SAT Problem." AAAI Conference on Artificial Intelligence, 2025. doi:10.1609/AAAI.V39I11.33228Markdown
[Liang et al. "DiverSAT: A Novel and Effective Local Search Algorithm for Diverse SAT Problem." AAAI Conference on Artificial Intelligence, 2025.](https://mlanthology.org/aaai/2025/liang2025aaai-diversat/) doi:10.1609/AAAI.V39I11.33228BibTeX
@inproceedings{liang2025aaai-diversat,
title = {{DiverSAT: A Novel and Effective Local Search Algorithm for Diverse SAT Problem}},
author = {Liang, Jiaxin and Zhou, Junping and Yin, Minghao},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {2025},
pages = {11290-11298},
doi = {10.1609/AAAI.V39I11.33228},
url = {https://mlanthology.org/aaai/2025/liang2025aaai-diversat/}
}