Computer Science
Computer Science
bullet Students, professional performers to present Shange’s production at Rowan | More

bullet Quest of a lifetime: Film prof nets $100K MacArthur grant | More

bullet Rowan students will cha-cha For CHOP | More

bullet U.S. Rep. John Conyers to deliver 2016 Rosa Parks Luncheon keynote address | More

bullet ‘Downton Discussions’ to shed light on PBS series’ final season | More

Computer Science Seminar Series

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 [] 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.