Computer Science
Computer Science
bullet Rowan hosts Attracting Women into Engineering for middle school girls | More

bullet “My Little Hundred Million”: Best-selling author’s podcast celebrates Henry Rowan, explores higher ed philanthropy | More

bullet Rowan student journalists to cover Democratic National Convention | More

bullet Rowan’s Online Construction Management degree cited as a “best value” | More

bullet Rowan Engineering welcomes BEST young men | 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.