ParSAT

Project Proposal

Summary of Work

In the past few weeks, we have done some research on SAT solvers and implemented a working sequential version with multiple optimizations, such as ruling out potential solutions that cannot be satisfied, as well as definitively assigning specific values to literals in one-clause statements. We also wrote a random SAT expression generator in order to easily generate large expressions and measure the time it takes to find whether the expressions are satisfiable or not. We’ve also begun work on achieving parallelism on checking individual solutions with single threads.

Revised Schedule

Expected Goals and Deliverables

Our expected goals and deliverables have not changed very much, but we will need to speed up our current rate of progress to obtain the stated parallel goals. Our reach goal remains getting our SAT solver to work on multiple machines or cores, which would be nice to have. Another goal we’d like to hit for the parallelism competition is to perhaps cache the results of different clauses so we don’t need to repeat work each time (since the result of each clause is independent of other clauses). It might also be interesting to explore how we could vectorize the clauses to perform SIMD and speed up our computations further.

Parallelism Competition

We would like to show a graph of our speedups compared to our initial sequential implementation, with gradually improving performance as we improve our attempts to achieve an efficient parallel solution. We’d also like to demo our SAT solver on million-clause SAT expressions, if we are able to speed up our SAT solver to that extent.

Results

We created a random clause generator that accepts as input the number of variables, number of clauses, and maximum clause length. Our benchmark for the sequential version will have variances in these 3 values. For reference however, our sequential solution on 10 variables, 10000 clauses, and a maximum clause length of 5 takes around 10 seconds. With 15 variables, the time goes up to 1 minute, 25 seconds. Our time slows drastically when we increase the number of variables due to the rapidly increasing number of possible solutions there could be, so we’ll be working to improve that time with parallelism techniques.

Concerns

Our primary concern is being able to finish all the parallel goals we have stated in our schedule, primarily because it took so long for us to decide on a project, so as a result, we don’t have as much parallelism currently as we expected. I believe our project now is primarily a matter of going through our remaining goals and discussing how exactly we should synchronize and split the work among different threads to achieve good performance.