Project Description: goals and purpose of the project
Our goal was to develop an open-source, multithreaded, parallel solver of the Satisfiability (SAT) problem, implemented in Java for a multi-core personal computer. The classic NP-complete problem of SAT is defined as follows: Given a propositional logic formula in conjunctive normal, is there an assignment of true/false values to the variables in the formula that makes the formula evaluate to true? The vast majority of the personal computers that are being sold today possess more than one processor. Moreover, most modern operating systems are multithreaded in nature and provide users the capability of writing multithreaded applications. If a problem may be attacked in a multithreaded manner and the execution of each thread can be delegated to one of the available processor, we are more than likely to solve the problem faster.
Process used on the project
We developed Msat, a multithreaded SAT solver in Java, and conducted performance studies. iIn the initial stages of our project, we studied SAT in great detail. We also developed a multi-threaded Java application and a simple SAT solver. We integrated both into a prototype multithreaded SAT solver called Msat. At this stage, Msat was designed to run on a dual-core machine.
Once this was accomplished, we began to conduct performance studies on Msat. In order to carry this out, we needed a dependable operating system as we are relying on the operating system, solely, to assign threads to the processors. Therefore, we chose to run our program on a 4-processor Sun Ultra Spark II running Sun OS.
Next, we worked collaboratively with Rowan SIGSAT (Special Interest Group on SAT) members and adapted one of their DLL solvers to use with Msat. This DLL solver implements unit propagation and the Two-sided Jeroslaw-Wang heuristic.
With this we began to do more performance studies. We found that our nave problem splitting method and heavy communication overhead caused Msat to be inefficient.
During this time, we presented our project at a Rowan University Computer Science Seminar. We also presented posters at CCSCNE 2008, where we won 2nd place, and Rowan University's STEM Symposium.
For the next version, we reworked Msat to reduce the communication overhead between Msat and the different solvers. We implemented a second split algorithm based on the Two-Sided Jeroslaw-Wang weights. We obtained performance results for this improved algorithm and implementation.
Conclusions
We collected performance studies on Msat with the DLL solver with different values for the number of subproblems parameter. We compared these results to those of the DLL solver running on its own. The input problems that we used were obtained from satlib.org. The files that begin with "s" are satisfiable and the files that begin with "u" are unsatisfiable. The first number in the file name specifies the number of variables in the problem.
The resulting runtimes are shown in the table below. Msat with our DLL solver can solve larger problems (about 100 variables) and medium problems (about 75 variables) faster than our DLL solver alone. Msat with a brute-force solver and the DLL solver alone have comparable results for smaller (about 25 variables) problems (these results are not shown). The results so far do not indicate our optimum value for the number of subproblems parameter. The end result was successful in that Msat performed faster than a solver running on a single processor. 
On our website you will find information on Project documents (Proposal, Mid-Year Progress Report, Final Report, and Weekly Summaries), a .jar file containing our Java code, Javadoc, a Readme file on how to run our program and our performance results.
Websites Developed and Publications
Web pages developed:
- Danielle Socha and Andrea F. Lobo, "A Multi-threaded SAT Solver," Second Place at the Student Poster Competition of the Thirteenth Annual CCSC Northeastern Conference, April 2008.
- Danielle Socha, Greg Viola, Andrew Fabian and Andrea F. Lobo, "A Multithreaded SAT Solver," Student poster presentation at the 2008 Rowan University STEM Symposium, April 2008.
- Msat at http://elvis.rowan.edu/~eckard73/CREU_SAT/SATWeb.htm. Accessed 2008/05/13.
- Invited talk: Danielle Socha, "A Multithreaded SAT Solver," Rowan Univeristy Computer Science Seminar Series, April 9th, 2008.
- Receipient of the 2008 Dean's Tea Award for Undergraduate Excellence, Rowan University, College of Liberal Arts and Sciences, April 2008.
Back to 2007-2008 Project Listing