When Making the Problem Smaller Can Also Make it Harder: Partitioning for Parallel Satisfiability Modulo Theories
Amalee Wilson, Stanford University
How can quantum programs be most effectively mapped to quantum hardware? What is the best way to schedule jobs on a machine with limited resources while ensuring that users cannot access the resources and data of others? And how can we prove the equivalence of two programs when porting software to a new system? These problems can be mathematically formulated as systems of constraints and solved by a computer using a Satisfiability Modulo Theories (SMT) solver. Given a system of constraints, the SMT solver tries to find values for the variables to satisfy the constraints, or it will determine that no such values exist. SMT solving is a relatively new technology that is currently under-utilized in high performance computing (HPC). One primary barrier to SMT solvers’ widespread adoption is execution time. Finding solutions to a complex set of constraints is computationally difficult, so even the best SMT solvers require a great deal of time to process large problems. In HPC, though, we have a solution for hard problems: parallelize the work. However, partitioning an SMT problem for parallel solving is much more complicated than a traditional divide-and-conquer approach. Partitioning is difficult due to the nature of state-of-the-art algorithms for SMT solving. SMT solvers perform a type of search over the problem space, and information computed in one part of the search space can affect the exploration of other areas of the space. For problems that have no solution (those which the solver would report as unsatisfiable), partitioning can result in a linear slowdown with respect to the number of partitions. My work focuses on developing more effective partitioning algorithms and execution strategies for parallel SMT solving. This poster presents partitioning algorithms for SMT problems, data on the performance of those partitioning algorithms, and challenges involved with parallelizing SMT solving.
Abstract Author(s): Amalee Wilson