The road to improving the performance of satisfiability solvers using HPC

Boolean Satisfiability (SAT) solvers have become an enabling technology for diverse application areas of military and commercial interest. A Phase H Small Business Innovation Research project under the Architectures for Cognitive Information Processing (ACIP) program has developed novel problem representations, algorithms, and heuristics to improve SAT solver performance over existing approaches. Reservoir Labs has parallelized a SA T solver for the Cray XD1, writing fine grained messaging layers over Message Passing Interface (MPI). The solver is written in a message-driven computing style. We partition the problem over the nodes of the XD1 to achieve concurrency in the propagation of implications. We have facilities to partition the clause database over the nodes to improve locality of reference. A tool, Salt, can translate a high level logic language into SAT problem instances and transmit partition and heuristic information into the solver. We report on the current capability and performance of the solver, and in particular the tradeoff between locality and concurrency in our system. Finally, we point to the forward roadmap to achieving greater performance on this problem.