Accelerating Boolean Satisfiability on a Graphics Processing Unit

作者: Kanupriya Gulati , Sunil P Khatri , Kanupriya Gulati , Sunil P Khatri

DOI: 10.1007/978-1-4419-0944-2_6

关键词:

摘要: In this chapter we present a Boolean satisfiability solver with new GPU-enhanced variable ordering heuristic. Our approach is implemented in CPU-based procedure and leverages the parallelism of graphics processing unit (GPU). The CPU implements complete (MiniSAT), while GPU an approximate (an implementation survey propagation – SurveySAT).

参考文章(18)
Panagiotis Manolios, Yimin Zhang, Implementing Survey Propagation on Graphics Processing Units Lecture Notes in Computer Science. pp. 311- 324 ,(2006) , 10.1007/11814948_30
Yi Shang, Benjamin W. Wah, A Discrete Lagrangian-Based Global-SearchMethod for Solving Satisfiability Problems Journal of Global Optimization. ,vol. 12, pp. 61- 99 ,(1998) , 10.1023/A:1008287028851
HoonSang Jin, Mohammad Awedh, Fabio Somenzi, CirCUs: A Satisfiability Solver Geared towards Bounded Model Checking Computer Aided Verification. pp. 519- 522 ,(2004) , 10.1007/978-3-540-27813-9_50
Peter J. Stuckey, Lei Zheng, Improving SAT using 2SAT ACSC '02 Proceedings of the twenty-fifth Australasian conference on Computer science - Volume 4. ,vol. 24, pp. 331- 340 ,(2002) , 10.1145/563857.563839
Wahid Chrabakh, Rich Wolski, GridSAT Proceedings of the 2003 ACM/IEEE conference on Supercomputing - SC '03. pp. 37- 37 ,(2003) , 10.1145/1048935.1050188
R. Zecchina, M. Mézard, A. Braunstein, Survey propagation: An algorithm for satisfiability Random Structures and Algorithms. ,vol. 27, pp. 201- 226 ,(2005) , 10.1002/RSA.V27:2
Cyril Furtlehner, Riccardo Zecchina, Marc Mézard, Joël Chavas, Survey-propagation decimation through distributed local computations Journal of Statistical Mechanics: Theory and Experiment. ,vol. 2005, pp. 11016- ,(2005) , 10.1088/1742-5468/2005/11/P11016
Max Böhm, Ewald Speckenmeyer, A fast parallel SAT-solver — efficient workload balancing Annals of Mathematics and Artificial Intelligence. ,vol. 17, pp. 381- 400 ,(1996) , 10.1007/BF02127976
Karem A. Sakallah, João P. Marques Silva, GRASP—a new search algorithm for satisfiability international conference on computer aided design. pp. 220- 227 ,(1996) , 10.5555/244522.244560
Donald Loveland, George Logemann, Martin Davis, A machine program for theorem-proving ,(2011)