Parallel Multithreaded Satisfiability Solver
作者： Yulik Feldman , Nachum Dershowitz , Ziyad Hanna
DOI: 10.1016/J.ENTCS.2004.10.020
关键词:
摘要: We describe the design and implementation of a highly optimized, multithreaded algorithm for propositional satisfiability problem. The is based on Davis-Putnam-Logemann-Loveland sequential algorithm, but includes many optimization techniques introduced in recent years. provide experimental results execution parallel variety multiprocessor machines with shared memory architecture. In particular, detrimental effect performance processor cache studied.
core.ac.uk
elsevier.com
sci-hub.se 参考文章(23)
Bart Selman, Henry Kautz, Blackbox: Unifying sat-based and graph-based planning international joint conference on artificial intelligence. ,(1999)
Conor F. Madigan, Lintao Zhang, Sharad Malik, Matthew W. Moskewicz, Ying Zhao, Cha : Engineering an e cient SAT solver design automation conference. ,(2001)
Simone L. Martins, Celso C. Ribeiro, Mauricio C. Souza, A Parallel GRASP for the Steiner Problem in Graphs Lecture Notes in Computer Science. pp. 285- 297 ,(1998) , 10.1007/BFB0018547
João Marques-Silva, The Impact of Branching Heuristics in Propositional Satisfiability Algorithms portuguese conference on artificial intelligence. pp. 62- 74 ,(1999) , 10.1007/3-540-48159-1_5
Benjamin W. Wah, Paul W. Purdom, John Franco, Jun Gu, Algorithms for the Satisfiability (SAT) Problem: A Survey, Satisfiability Problem: Theory and Applications. pp. 19- 151 ,(1996)
M.N. Velev, R.E. Bryant, Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors design automation conference. pp. 226- 231 ,(2001) , 10.1109/DAC.2001.156140
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
David A. Plaisted, Steven Greenbaum, A Structure-preserving Clause Form Translation Journal of Symbolic Computation. ,vol. 2, pp. 293- 304 ,(1986) , 10.1016/S0747-7171(86)80028-1
Roland T. Chin, Charles R. Dyer, Model-based recognition in robot vision ACM Computing Surveys. ,vol. 18, pp. 67- 108 ,(1986) , 10.1145/6462.6464
Stephen A. Cook, The complexity of theorem-proving procedures symposium on the theory of computing. pp. 151- 158 ,(1971) , 10.1145/800157.805047