PaMiraXT 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 Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year PaMiraXT: parallel SAT solving with threads and message passing. Zbl 1190.68057Schubert, Tobias; Lewis, Matthew; Becker, Bernd 2009 all top 5 Cited by 34 Authors 3 Becker, Bernd 2 Lewis, Matthew D. T. 2 Schubert, Tobias 2 Semenov, Aleksandr Anatol’evich 1 Abreu, Salvador 1 Ahmed, Tanbir 1 Burchard, Jan 1 Caniou, Yves 1 Codognet, Philippe 1 Czutro, Alexander 1 Diaz, Daniel 1 Engelke, Piet 1 Gent, Ian Philip 1 Hyvärinen, Antti E. J. 1 Ignat’ev, A. S. 1 Ignatyev, Alexey A. 1 Junttila, Tommi A. 1 Kullmann, Oliver 1 Lynce, Inês 1 Manquinho, Vasco M. 1 Martins, Ruben 1 McCreesh, Ciaran 1 Miguel, Ian 1 Moore, Neil C. A. 1 Niemelä, Ilkka N. F. 1 Nightingale, Peter W. 1 Polian, Ilia 1 Prosser, Patrick 1 Reddy, Sudhakar M. 1 Richoux, Florian 1 Sanders, Peter 1 Schreiber, Dominik 1 Snevily, Hunter S. 1 Unsworth, Chris all top 5 Cited in 7 Serials 2 Constraints 1 Discrete Applied Mathematics 1 International Journal of Parallel Programming 1 Fundamenta Informaticae 1 Theory and Practice of Logic Programming 1 Journal of Satisfiability, Boolean Modeling and Computation 1 Prikladnaya Diskretnaya Matematika Cited in 5 Fields 9 Computer science (68-XX) 2 Operations research, mathematical programming (90-XX) 1 Mathematical logic and foundations (03-XX) 1 Combinatorics (05-XX) 1 Information and communication theory, circuits (94-XX) Citations by Year