SHF: Small: CoopSLS: Improving Boolean Satisfiability Solvers through Cooperative Stochastic Local Search

Carnegie Mellon University, Pittsburgh PA

Investigators

Abstract

Automated reasoning based on Boolean Satisfiability (SAT) solving has emerged as a powerful technology to solve a wide range of problems, including verification, planning, and mathematical challenges. Reasoning algorithms for SAT solving are generally categorized into two types: complete search and local search. Complete search, e.g., conflict-driven clause learning (CDCL), systematically explores the entire search space, whereas local search uses randomization and heuristics to guide the search process, e.g., stochastic local search (SLS). The current best solvers use a portfolio approach where multiple different solvers are employed to solve a given SAT instance, but there is no deeper exchange of information between the solvers. This project identifies strategies for switching between solvers when combining solvers. More specifically, the research team innovatively combines local search algorithms for SAT solving to enable their cooperation. The project develops three automated reasoning frameworks. The first framework enhances cooperation within a sequential solver by leveraging the complementary performance and structural commonalities of different algorithms. The second framework extends this cooperation to a parallel level, where a diverse suite of algorithms collaborates towards a common solution. Finally, the project integrates complete search into the cooperation to merge both traditional types of reasoning into a single powerful parallel framework to solve new challenging problems. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.