Journal on Satisfiability, Boolean Modeling and Computation - Volume 6, issue 4

Authors: Schubert, Tobias | Lewis, Matthew | Becker, Bernd

Article Type: Research Article

Abstract: 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. Show more

Keywords: parallel SAT solving, threads, message passing

DOI: 10.3233/SAT190068

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 6, no. 4, pp. 203-222, 2010

Authors: Hyvärinen, Antti E.J. | Junttila, Tommi | Niemelä, Ilkka

Article Type: Research Article

Abstract: Computational Grids provide a widely distributed computing environment suitable for randomized SAT solving. This paper develops techniques for incorporating clause learning, known to yield significant speed-ups in the sequential case, in such a distributed framework. The approach exploits existing state-of-the-art clause learning SAT solvers by embedding them with virtually no modifications. The paper presents an algorithmic framework for learning-enhanced randomized SAT solving in Grid environments. With a substantial amount of controlled experiments it is demonstrated that this approach enables a form of clause learning which is not directly available in the underlying sequential SAT solver. Finally, an implementation of the …algorithm is run in a production level Grid where it solves several problems not solved in the SAT 2007 solver competition. Show more

Keywords: propositional satisfiability, SAT solvers, clause learning, randomized search, distributed computing, computational grids

DOI: 10.3233/SAT190069

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 6, no. 4, pp. 223-244, 2010

Authors: Hamadi, Youssef | Jabbour, Said | Sais, Lakhdar

Article Type: Research Article

Abstract: In this paper, ManySAT a new portfolio-based parallel SAT solver is thoroughly described. The design of ManySAT benefits from the main weaknesses of modern SAT solvers: their sensitivity to parameter tuning and their lack of robustness. ManySAT uses a portfolio of complementary sequential algorithms obtained through careful variations of the standard DPLL algorithm. Additionally, each sequential algorithm shares clauses to improve the overall performance of the whole system. This contrasts with most of the parallel SAT solvers generally designed using the divide-and-conquer paradigm. Experiments on many industrial SAT instances, and the first rank obtained by ManySAT in the parallel track …of the 2008 SAT-Race clearly show the potential of our design philosophy. Show more

Keywords: parallel search, dynamic restarts, extended clause learning

DOI: 10.3233/SAT190070

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 6, no. 4, pp. 245-262, 2010

Authors: Hamadi, Youssef

Article Type: Editorial

DOI: 10.3233/SAT190071

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 6, no. 4, pp. 263-263, 2010