Strategies for Solving SAT in Grids by Randomized Search

Grid computing offers a promising approach to solving challenging computational problems in an environment consisting of a large number of easily accessible resources. In this paper we develop strategies for solving collections of hard instances of the propositional satisfiability problem (SAT) with a randomized SAT solver run in a Grid. We study alternative strategies by using a simulation framework which is composed of (i) a grid model capturing the communication and management delays, and (ii) run-time distributions of a randomized solver, obtained by running a state-of-the-art SAT solver on a collection of hard instances. The results are experimentally validated in a production level Grid. When solving a single hard SAT instance, the results show that in practice only a relatively small amount of parallelism can be efficiently used; the speedup obtained by increasing parallelism thereafter is negligible. This observation leads to a novel strategy of using grid to solve collections ...

• Type: Conference
• Year: 2008
• Where: AISC
• Authors: Antti Eero Johannes Hyvärinen, Tommi A. Junttila, Ilkka Niemelä
• Keywords: AISC 2008, Artificial Intelligence, Hard Instances, Randomized Sat Solver, Sat Solver