CCCA Showcase a focus on talent, achievement | More
Rowan Engineers Without Borders works with elementary school students on engineering-related projects | More
COMMENTARY: Restructuring good for Rowan, N.J. | More
Making the PACT and Taking Back the Night | More
Student debaters from six colleges look to win first-ever South Jersey Criminal Justice Debate Invitational at Rowan | More
Using general trees insight to efficiently visualize large networks
By Danielle Socha, CS 08
Date: Wednesday April 9, 2008
Time: 11:00- 12:00
Place: Robinson 101A
The classic NP-complete problem of SAT [GaJo1979] is defined as follows:
Given a propositional logic formula in conjunctive normal form, is there an assignment of true/false values to its variables that makes the formula evaluate to true? Significant research and practical work exists on SAT. Efficient, proprietary Sat solvers exist for industrial use in many application domains [EaTr2001, MaEA2003].The SIM testbed [GiEA2001] is an open-source, easy to use library of efficient, sequential procedures for SAT solvers that contains C implementations of several well-known SAT algorithms and heuristics. SATLIB [satlib.org] maintains public domain repositories of benchmark solvers and “hard” SAT instances. Existing parallel solvers are not public domain or use a complex distributed computing infrastructure [ChWo2006]. Additionally, anyone can enter the annual SAT solver competition [satcomp].
We are developing Msat to take advantage of increasingly common multiprocessor desktop computers. Msat is a multithreaded SAT solver, implemented in Java for a dual-core computer. It starts by creating two SAT solvers, each executing as a thread on a processor. Msat splits the input SAT problem into multiple subproblems. It assigns the subproblems sequentially to the solvers until either a solution is found, or all subproblems have been processed and no solution exists.
The working version of Msat uses a simple solver, is modular and supports heterogeneous solvers. We are redesigning the Msat-solver interface so that Msat can use any solver that accepts input in the International SAT Competitions format [satcomp]. The SIGSAT research group has working versions developed DLL [DaEA1962, BaSc1997] solver modules with unit propagation [ZhSt2000]. We plan to conduct a performance study of Msat with these, and possibly other, solvers on a suite of input problems. We posit that the execution times of the two-processor Msat will be faster than those of traditional single-processor solvers. We are committed to making the Msat source publicly available. Future work may include extensions for computers with more processors and for distributed solvers.