Title :
Communication in Massively-Parallel SAT Solving
Author :
Ehlers, Thorsten ; Nowotka, Dirk ; Sieweck, Philipp
Author_Institution :
Dept. of Comput. Sci., Univ. Kiel, Kiel, Germany
Abstract :
The exchange of learnt clauses is a key feature in parallel SAT solving. We present an approach based on a communication graph. Each solver thread corresponds to a node in this graph. Communication between two solvers is allowed if the respective nodes are connected by an edge. This yields another dimension in controlling the amount of communication. We show results for this approach, gaining significant speedups for up to 256 parallel solvers.
Keywords :
Boolean functions; computability; graph theory; Boolean satisfiability; communication graph; parallel SAT solving; solver thread; Benchmark testing; Computer architecture; Databases; Hardware; Portfolios; Sugar; Topology; Distributed Computing; High Performance Computing; Portfolio; Satisfiability;
Conference_Titel :
Tools with Artificial Intelligence (ICTAI), 2014 IEEE 26th International Conference on
Conference_Location :
Limassol
DOI :
10.1109/ICTAI.2014.111
