SATDiv: An Effective Solver for Diverse SAT Problem

Abstract

The Boolean Satisfiability problem (SAT) is a fundamental problem in computer science. While standard SAT solvers focus on finding a single solution, domains such as semiformal verification and software testing require generating multiple, diverse solutions to enhance testing effectiveness. Particularly in semiformal verification, utilizing such diverse solutions has proven effective in uncovering latent errors in complex designs that evade simulation and formal verification. This requirement gives rise to the Diverse SAT problem, which aims to generate a set of k solutions with the sum of pairwise Hamming distances as large as possible. In this paper, we present SATDiv, an advanced solver designed to effectively address the Diverse SAT problem. We conducted extensive experiments on public benchmarks derived from real-world applications in both hardware semiformal verification and software testing. The experimental results demonstrate that SATDiv outperforms state-of-the-art Diverse SAT solvers.