We investigate parallel search algorithms for the Satisfiability (SAT) problem—with Boolean SAT widely recognised as the first and canonical NP-Complete problem. Such algorithms have broad applications across domains such as computer security, cryptology, bioinformatics, spectrum auction design, formal verification, and automated planning. We will briefly motivate and describe a class of pseudo-Boolean SAT problems.

SAT problems are typically approached using two primary search paradigms: systematic search and stochastic local search. In this talk, we focus on a contemporary variant of the latter—continuous local search—an approach amenable to execution and acceleration via parallelisation on GPUs. We will discuss how to leverage JAX - a high-performance numerical computing library-to accelerate and scale key components of continuous local search using GPU parallelism. This will show how JAX can be used to efficiently implement and experiment with parallel search algorithms for evaluating SAT.