swMATH ID: 6997
Software Authors: Schubert, Tobias; Lewis, Matthew; Becker, Bernd
Description: PaMiraXT: parallel SAT solving with threads and message passing. 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.
Homepage: http://jsat.ewi.tudelft.nl/content/volume6/JSAT6_10_Schubert.pdf
Related Software: ManySAT; Lingeling; MiniSat; Plingeling; Chaff; SATO; PSATO; MPI; GridSAT; HordeSat; Treengeling; COMET; antom; c-sat; ZetaSAT; PMSat; PrecoSAT; PicoSAT; PaQuBE; BerkMin
Cited in: 11 Publications

Citations by Year