Schubert, Tobias; Lewis, Matthew; Becker, Bernd PaMiraXT: parallel SAT solving with threads and message passing. (English) Zbl 1190.68057 J. Satisf. Boolean Model. Comput. 6, No. 4, 203-222 (2009). Summary: This article describes PaMiraXT, a powerful parallel SAT algorithm. PaMiraXT follows a master/client model based on message passing, making it suitable for any kind of workstation cluster. For the clients, MiraXT is used, which itself is thread-based parallel solver designed to take advantage of current and future shared memory multiprocessor systems. We highlight design and implementation details that allow the threads/clients to run and cooperate efficiently. Experimental results show that MiraXT compares well to other state-of-the-art SAT algorithms. In single-threaded mode, it outperforms MiniSat2, PicoSAT 535, and RSat 2.01, while in multi-threaded mode, MiraXT provides cutting edge performance, as it solves significantly more instances within the given time limit. A case study, using three copies of MiraXT with a total of 8 threads as clients, underlines the potential of PaMiraXT, resulting in a speedup of 5.62 on the industrial benchmarks of the 2007 SAT competition. Cited in 9 Documents MSC: 68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) 68W10 Parallel algorithms in computer science Software:Chaff; PSATO; BerkMin; PaMiraXT; MPI/MPICH; SATO; MiniSat PDFBibTeX XMLCite \textit{T. Schubert} et al., J. Satisf. Boolean Model. Comput. 6, No. 4, 203--222 (2009; Zbl 1190.68057)