Partitioning SAT Instances for Distributed Solving

Abstract. In this paper we study the problem of solving hard propositional satisfiability problem (SAT) instances in a computing grid or cloud, where run times and communication between parallel running computations are limited. We study analytically an approach where the instance is partitioned iteratively into a tree of subproblems and each node in the tree is solved in parallel. We present new methods which combine clause learning and look-ahead to construct partitions, evaluate their efficiency experimentally, and finally demonstrate the power of the approach in a real grid environment by solving several instances that were not solved in a SAT solver competition.

• Type: Journal
• Year: 2010
• Where: LPAR
• Authors: Antti Eero Johannes Hyvärinen, Tommi A. Junttila, Ilkka Niemelä
• Keywords: Automated Reasoning, Hard Propositional Satisfiability, LPAR 2010, Parallel Running Computations, Real Grid Environment