By Eileen Jiang (yuanj) and Ashley Lai (ahlai)
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.
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 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.
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 ChoiceWe will be implementing the parallel SAT solver with Intel Xeon Phi’s to take advantage of the large number of cores and to explore the OMP library. We will be using the latedays cluster to access the Xeon Phi’s that we also used for the ParaGraph assignment.
ScheduleTuesday, April 5 - Revise project proposal
Sunday, April 10 - Implement sequential version
Friday, April 15 (CHECKPOINT) - Achieve parallelism by checking individual solutions with single threads
Friday, April 22 - Achieve parallelism by using multiple threads to check a single solution
Friday, April 29 - If time allows, attempt several of our reach goals (for example, implement our algorithm on multiple cores)
Friday, May 6 - Prepare presentation