2010 | OriginalPaper | Chapter
Partitioning SAT Instances for Distributed Solving
Authors : Antti E. J. Hyvärinen, Tommi Junttila, Ilkka Niemelä
Published in: Logic for Programming, Artificial Intelligence, and Reasoning
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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 for constructing partitions which combine clause learning and lookahead. The methods are incorporated into the iterative approach and its performance is demonstrated with an extensive comparison against the best sequential solvers in the SAT competition 2009 as well as against two efficient parallel solvers.