On the parallelization of SAT solvers

作者: Yasmeen Abd El Khalek , Mona Safar , M. Watheq El-Kharashi

DOI: 10.1109/ICCES.2015.7393031

关键词:

摘要: This paper presents the main challenges, hot topics, and intriguing issues in area of parallel SAT solving which provides possible directions for future research. It gives a detailed summary features technologies used most widely known successful solvers shows strong points shortcomings them. In addition, it compares between basic characteristics these including algorithms, architecture paradigm, scalability, network communication, managing workload distribution more. Finally, new approach is proposed that expected to be very promising direction as copes with nature paradigm results almost linear speedup instances, independent number variables formula.

参考文章(30)
Gilles Audemard, Laurent Simon, Lazy Clause Exchange Policy for Parallel SAT Solvers theory and applications of satisfiability testing. pp. 197- 205 ,(2014) , 10.1007/978-3-319-09284-3_15
Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel, Sanjit A. Seshia, Moshe Y. Vardi, On Parallel Scalable Uniform SAT Witness Generation Tools and Algorithms for the Construction and Analysis of Systems. ,vol. 9035, pp. 304- 319 ,(2015) , 10.1007/978-3-662-46681-0_25
Tomáš Balyo, Peter Sanders, Carsten Sinz, HordeSat: A Massively Parallel Portfolio SAT Solver theory and applications of satisfiability testing. pp. 156- 172 ,(2015) , 10.1007/978-3-319-24318-4_12
Kei Ohmura, Kazunori Ueda, c-sat: A Parallel SAT Solver for Clusters theory and applications of satisfiability testing. pp. 524- 537 ,(2009) , 10.1007/978-3-642-02777-2_47
Matthew Lewis, Paolo Marin, Tobias Schubert, Massimo Narizzano, Bernd Becker, Enrico Giunchiglia, PaQuBE: Distributed QBF Solving with Advanced Knowledge Sharing theory and applications of satisfiability testing. pp. 509- 523 ,(2009) , 10.1007/978-3-642-02777-2_46
Luís Gil, Paulo Flores, Luís Miguel Silveira, PMSat: a parallel version of MiniSAT Journal on Satisfiability, Boolean Modeling and Computation. ,vol. 6, pp. 71- 98 ,(2008) , 10.3233/SAT190063
Kuldeep Singh Meel, Sampling Techniques for Boolean Satisfiability arXiv: Logic in Computer Science. ,(2014)
Wahid Chrabakh, Rich Wolski, GridSAT Proceedings of the 2003 ACM/IEEE conference on Supercomputing - SC '03. pp. 37- 37 ,(2003) , 10.1145/1048935.1050188
Bernard Jurkowiak, Chu Min Li, Gil Utard, Parallelizing Satz Using Dynamic Workload Balancing Electronic Notes in Discrete Mathematics. ,vol. 9, pp. 174- 189 ,(2001) , 10.1016/S1571-0653(04)00321-X