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.

References in zbMATH (referenced in 12 articles , 1 standard article )

Showing results 1 to 12 of 12.
Sorted by year (citations)

  1. Schreiber, Dominik; Sanders, Peter: Scalable SAT solving in the cloud (2021)
  2. Gent, Ian P.; Miguel, Ian; Nightingale, Peter; McCreesh, Ciaran; Prosser, Patrick; Moore, Neil C. A.; Unsworth, Chris: A review of literature on parallel constraint solving (2018)
  3. Burchard, Jan; Schubert, Tobias; Becker, Bernd: Laissez-faire caching for parallel #SAT solving (2015)
  4. Caniou, Yves; Codognet, Philippe; Richoux, Florian; Diaz, Daniel; Abreu, Salvador: Large-scale parallelism for constraint-based local search: the costas array case study (2015)
  5. Ahmed, Tanbir; Kullmann, Oliver; Snevily, Hunter: On the van der Waerden numbers (\mathrmw(2; 3, t)) (2014)
  6. Martins, Ruben; Manquinho, Vasco; Lynce, Inês: An overview of parallel SAT solving (2012)
  7. Hyvärinen, Antti E. J.; Junttila, Tommi; Niemelä, Ilkka: Partitioning search spaces of a randomized search (2011)
  8. Ignatiev, Alexey; Semenov, Alexander: DPLL+ROBDD derivation applied to inversion of some cryptographic functions (2011)
  9. Czutro, Alexander; Polian, Ilia; Lewis, Matthew; Engelke, Piet; Reddy, Sudhakar M.; Becker, Bernd: Thread-parallel integrated test pattern generator utilizing satisfiability analysis (2010)
  10. Ignat’ev, A. S.; Semenov, A. A.: Algorithms using ROBDD as a base for Boolean constraints (2010)
  11. Schulz, Sven; Blochinger, Wolfgang: Parallel SAT solving on peer-to-peer desktop grids (2010) ioport
  12. Schubert, Tobias; Lewis, Matthew; Becker, Bernd: PaMiraXT: parallel SAT solving with threads and message passing (2009)