TCS / Research / Publications / SATU: A System for Distributed Propositional Satisfiability Checking in Computational Grids
Helsinki University of Technology, 
     Laboratory for Theoretical Computer Science

SATU: A System for Distributed Propositional Satisfiability Checking in Computational Grids

Reference:

Antti E. J. Hyvärinen. SATU: A system for distributed propositional satisfiability checking in computational grids. Research Report A100, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, February 2006.

Abstract:

In addition to data storage and indexing systems, computational grids are used for solving computationally demanding tasks. Because of the inherent communication delays and high failure probabilities of a loosely coupled and large computational grid, such an environment poses a great challenge for highly data-dependent algorithms. In this work we present a distribution scheme for solving propositional satisfiability problem (SAT) instances, called scattering. The key advantages of scattering are that it can be used in conjunction with any sequential or parallel satisfiability checker, including industrial black box checkers, and that the distribution heuristic is strictly separated from the heuristic used in sequential solving. We also give an implementation of the scheme and benchmark it using a production-level grid. The benchmarks range from factorization to cryptanalysis and random 3SAT. Some benchmarks not known to have been solved previously are solved with the distribution scheme.

Scattering is analysed with respect to the challenges posed by the grid environment: the long communication delays and the high failure rates of individual jobs. We study different approaches to coping with the communication delays and thus maximizing the effective parallelism in the grid. We give a criterion for the completeness of the scattering in a pure grid environment with failures.

Keywords:

Parallel Search Algorithms, Parallelization of DPLL procedure, Propositional Satisfiability, Computational Grid

Suggested BibTeX entry:

@techreport{HUT-TCS-A100,
    address = {Espoo, Finland},
    author = {Antti E. J. Hyv{\"a}rinen},
    institution = {Helsinki University of Technology, Laboratory for Theoretical Computer Science},
    month = {February},
    number = {A100},
    pages = {72},
    title = {{SATU}: A System for Distributed Propositional Satisfiability Checking in Computational Grids},
    type = {Research Report},
    year = {2006},
}

NOTE: Reprint of Master's thesis; see URL below.
PostScript (2 MB)
GZipped PostScript (602 kB)
PDF (685 kB)
See www.tcs.hut.fi ...

[TCS main] [Contact Info] [Personnel] [Research] [Publications] [Software] [Studies] [News Archive] [Links]
Latest update: 19 January 2010.