Computer Science
Computer Science
bullet Second biennial ScholarFest to celebrate Rowan research | More

bullet Rowan hosts talk on “Controlling Ebola Virus Outbreaks: A New Strategy to Block Virus Transmission and Spread” | More

bullet ‘Networking With Style’: Barefoot Cellars founders to discuss their road to wine-selling success during South Jersey Soiree | More

bullet Rowan science student will attend STEM conference in Jamaica | More

bullet Speakers to offer insights, inspiration during Disability Awareness Week at Rowan | 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.