ParSAT

Project Proposal

Title

ParSAT
By Eileen Jiang (yuanj) and Ashley Lai (ahlai)

Summary

We are going to write a parallel SAT solver that is compatible with any number of variables and clause size. We will be working on the latedays cluster to utilize the performance power of the Intel Xeon Phi.

Background

Our project involves working with the Intel Xeon Phi’s in order to speed up our computations. The main work comes from brute forcing all the possible solutions. The actual operations done on the elements are bitwise operators and thus shouldn’t take much computational time, but I believe that the main factor limiting good performance will be the sheer number of possibilities that we have to brute-force. As a result, the part of the solution that would benefit most from parallelism would be testing multiple possible solutions at once and “reducing” all the final results to determine whether the input expression is ultimately satisfiable or not.

The Challenge

The main challenge of writing a parallel SAT solver is figuring out the optimal way to brute-force as many possibilities as possible. Because the SAT problem is in NP, determining whether an expression is satisfiable takes an extremely long time to solve, depending on the size of the input. The part of the SAT solver that may be difficult to parallelize is communication across the different threads that run through the possible solutions to the SAT expression. Certain threads will return different answers to the satisfiability question, and so part of the challenge involves synchronizing the different results to output our desired final response.

In addition to implementing proper synchronization, there are also specific dependencies in the algorithm that we must account for. Earlier, we explored the idea of having each thread go through a possible solution and checking if that solution is satisfiable. Another idea would be to have multiple threads checking one possible solution, which could benefit especially if the SAT expression contains hundreds of thousands or millions of clauses. Part of the algorithm involves assigning boolean values to try out in a possible solution, so one dependency would be having to make sure to take care of this assignment first before seeing if it is actually satisfiable. Another possibility we could explore is which threads should take care of checking certain parts of the SAT expression to determine if that particular section is satisfiable or not. We would additionally need to make sure we synchronize correctly and efficiently when combining these results to determine if the possible SAT solution is actually satisfiable or not.

Resources

We have basic understanding of how a sequential SAT solver would work, and we’re planning to read up on different ways to optimize so that our algorithm doesn’t necessarily need to attempt every single brute force solution. We plan to discuss different ways to parallelize our starting sequential algorithm and look up different ideas online if all else fails. We’ll be starting from scratch on the latedays computers.

Goals and Deliverables

Plan to Achieve: We plan to achieve a parallelized version of the SAT solver that can determine satisfiability for a given SAT expression with single threads attempting individual solutions or multiple threads attempting single solutions. We would like to obtain something close to 10x speedup from the initial sequential version.

Hope to Achieve: If all goes well, we hope to achieve parallelism across multiple cores so that we can speedup our initial sequential version even more than 10x.

Our demo would likely be primarily focused around a live demo on a million-clause SAT expression (if our solver gets fast enough), as well as graphs demonstrating our speedups as we added in features that slowly improved our performance.

Platform Choice

Schedule