SATU: A SYSTEM FOR DISTRIBUTED PROPOSITIONAL SATISFIABILITY CHECKING IN COMPUTATIONAL GRIDS

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 productionlevel 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 gri