Computing diverse solutions for a given problem, in particular evolutionary diversity optimisation (EDO), is a hot research topic in the evolutionary computation community. This paper studies the Boolean satisfiability problem (SAT) in the context of EDO. SAT is of great importance in computer science and differs from the other problems studied in EDO literature, such as KP and TSP. SAT is heavily constrained, and the conventional evolutionary operators are inefficient in generating SAT solutions. Our approach avails of the following characteristics of SAT: 1) the possibility of adding more constraints (clauses) to the problem to forbid solutions or to fix variables, and 2) powerful solvers in the literature, such as minisat. We utilise such a solver to construct a diverse set of solutions. Moreover, maximising diversity provides us with invaluable information about the solution space of a given SAT problem, such as how large the feasible region is. In this study, we introduce evolutionary algorithms (EAs) employing a well-known SAT solver to maximise diversity among a set of SAT solutions explicitly. The experimental investigations indicate the introduced algorithms' capability to maximise diversity among the SAT solutions.

翻译：针对给定问题计算多样化解，尤其是进化多样性优化（EDO），是进化计算领域的研究热点。本文在EDO背景下研究布尔可满足性问题（SAT）。SAT在计算机科学中具有重要意义，且与EDO文献中研究的其他问题（如KP和TSP）存在显著差异：SAT具有强约束性，传统进化算子难以高效生成SAT解。我们的方法利用了SAT的以下特性：1）可向问题添加更多约束（子句）以禁止特定解或固定变量；2）现有文献中的强大求解器（如minisat）。我们借助此类求解器构建多样化解集。此外，最大化多样性可为我们提供关于给定SAT问题解空间的宝贵信息（例如可行域规模）。在本研究中，我们引入采用知名SAT求解器的进化算法（EAs），以显式最大化SAT解集间的多样性。实验研究表明，所提算法具备最大化SAT解多样性的能力。