GridSAT
- 15 November 2003
- proceedings article
- Published by Association for Computing Machinery (ACM)
Abstract
We present GridSAT, a parallel and complete satisfiability solver designed to solve non-trivial SAT problem instances using a large number of widely distributed and heterogeneous resources. The GridSAT parallel algorithm uses intelligent backtracking, distributed and carefully scheduled sharing of learned clauses, and clause reduction. Our implementation focuses on dynamic resource acquisition and release to optimize application execution. We show how the large number of computational resources that are available from a Grid can be managed effectively for the application by an automatic scheduler and effective implementation. GridSAT execution speed is compared against the best sequential solver as rated by the SAT2002 competition using a wide variety of problem instances. The results show that GridSAT delivers speed-up for all but one of the test problem instances that are of significant size. In addition, we describe how GridSAT has solved previously unsolved satisfiability problems and the domain science contribution these results make.Keywords
This publication has 17 references indexed in Scilit:
- Experiences with predicting resource performance on-line in computational grid settingsACM SIGMETRICS Performance Evaluation Review, 2003
- The GrADS Project: Software Support for High-Level Grid Application DevelopmentThe International Journal of High Performance Computing Applications, 2001
- Writing programs that run EveryWare on the Computational GridIEEE Transactions on Parallel and Distributed Systems, 2001
- PaSAT — Parallel SAT-Checking with Lemma Exchange: Implementation and ApplicationsElectronic Notes in Discrete Mathematics, 2001
- Parallelizing Satz Using Dynamic Workload BalancingElectronic Notes in Discrete Mathematics, 2001
- A comparative study of two Boolean formulations of FPGA detailed routing constraintsPublished by Association for Computing Machinery (ACM) ,2001
- The network weather service: a distributed resource performance forecasting service for metacomputingFuture Generation Computer Systems, 1999
- A constraint-based approach to narrow search trees for satisfiabilityInformation Processing Letters, 1999
- Netsolve: a Network-Enabled Server for Solving Computational Science ProblemsThe International Journal of Supercomputer Applications and High Performance Computing, 1997
- Improved deterministic test pattern generation with applications to redundancy identificationIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1989