Title

運用計算統一設備架構實現之平行化布爾可滿足性解法器

Translated Titles

Implementation of Parallel Boolean Satisfiability Solver by CUDA (Compute Unified Device Architecture)

DOI

10.6342/NTU.2011.01461

Authors

林拱民

Key Words

布爾可滿足性問題 ; 可滿足性解法器 ; 平行運算 ; 衝突驅使子句學習 ; 戴維斯-普特南-羅格曼-羅夫蘭 ; 通用計算於圖形處理單元 ; 計算統一設備架構 ; Boolean satisfiability problem ; satisfiability solver ; parallel computing ; SAT ; CDCL ; DPLL ; GPGPU ; CUDA

PublicationName

臺灣大學電子工程學研究所學位論文

Volume or Term/Year and Month of Publication

2011年

Academic Degree Category

碩士

Advisor

黃鐘揚

Content Language

英文

Chinese Abstract

解決布爾可滿足性問題在理論與工業應用上,扮演著極為關鍵角色。十五年來,布爾可滿足性解法器有著長足的進展,得以解決相當大型的問題。為了進一步解決更大型、更困難的布爾可滿足性問題,平行化布爾可滿足性解法器於近年來受到相當關注。最近幾年的國際布爾可滿足性解法器比賽之中,最佳的四至八線程平行化布爾可滿足性解法器的成績勝過最佳單線程布爾可滿足性解法器。 通用計算於圖形處理單元也在大量平行運算的領域之中興起。為了探討大量平行化布爾可滿足性解法器的概念,我們運用計算統一設備架構的平台,實現了名為「CUDASAT」的子句分享平行化、衝突驅使子句學習、戴維斯-普特南-羅格曼-羅夫蘭演算法布爾可滿足性解法器。 根據我們瞭解,目前尚未有類似CUDASAT的程式。實驗結果顯示,提昇平行解法器的數量時,平均每個解法器於搜尋上所用的步驟有著明顯下降的趨勢。CUDASAT的效能無法與現今最好的平行化布爾可滿足性解法器相比。它是作為發展大量平行化、低成本、替代性布爾可滿足性解法器的原型。

English Abstract

Boolean satisfiability (SAT) problem plays a critical role in theoretical and industrial applications. With the advance of SAT solvers in the past 15 years, we are capable to solve fairly large-scale problems. To improve the performance of SAT solvers for much larger and harder SAT problems, parallelization of SAT solvers is gaining much attention in recent years. The state-of-the-art 4-to-8 threaded parallel SAT solvers are more powerful than single-threaded ones in recent international SAT solver competitions. General-Purpose computation on Graphics Processing Units (GPGPU) is also emerging from massive parallel computing realm. To explore the concept of massive parallel SAT solvers, we have implemented the “CUDASAT”, a parallel CDCL-DPLL (Conflict Driven Clause Learning - Davis-Putnam-Logemann-Loveland) SAT solver with clause sharing on CUDA (Compute Unified Device Architecture) platform. To the best of our knowledge, CUDASAT is the first of its kind. The experimental results demonstrated a downward trend in average searching events per solver while increasing the number of parallel solver. While the performance is not comparable to those state-of-the-art parallel SAT solvers, CUDASAT serves as a prototype of massive parallelization toward an affordable and alternative solution for SAT solving.

Topic Category 電機資訊學院 > 電子工程學研究所
工程學 > 電機工程
Reference
  1. [1] Martin Davis and Hilary Putnam, “A computing procedure for quantification theory,” Journal of the ACM, vol.7, no.3, pp.201-215, July 1960.
    連結:
  2. [2] Martin Davis, Geoge Logemann, and Donald Loveland, “A machine program for theorem-proving,” Communications of the ACM, vol.5, no.7, pp.394-397, July 1962.
    連結:
  3. [4] Joao P. Marques-Silva and Karem A. Sakallah, “GRASP: a search algorithm for propositional satisfiability,” IEEE Transactions on Computers, vol.48, no.5, pp.506-521, May 1999.
    連結:
  4. [7] Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik, “Chaff: Engineering an Efficient SAT Solver,” Proceedings of Design Automation Conference, 2001., Las Vegas, Nevada, United States, pp.530-535, June 2001.
    連結:
  5. [14] Mary Sheeran and Gunnar Stalmarck, “A Tutorial on Stalmarck's Proof Procedure for Propositional Logic,” Formal Methods in Computer-Aided Design, Lecture Notes in Computer Science, vol.1522, pp.82-99, 1998.
    連結:
  6. [20] Sripriya G, Alan Bundy, and Alan Smaill, “Concurrent-Distributed Programming Techniques for SAT Using DPLL-Stalmarck,” International Conference on High Performance Computing & Simulation, 2009, Leipzig, Germany, pp.168-175, 2009.
    連結:
  7. [24] A. Braunstein, M. Mezard, and R. Zecchina, “Survey Propagation: An Algorithm for Satisfiability,” Random Structures & Algorithms, vol.27, no.2, pp.201-226, March 2005.
    連結:
  8. [34] Institute of Electrical and Electronics Engineers, Inc. (1996, October) IEEE Standards Interpretations for IEEE Std 1003.1c-1995. [Online]. http://standards.ieee.org/findstds/interps/1003-1c-95_int/index.html
    連結:
  9. [43] Lintao Zhang, Conor F. Madigan, Matthew H. Moskewicz, and Sharad Malik, “Efficient conflict driven learning in a boolean satisfiability solver,” Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, San Jose, California, United States, pp.279-285, 2001.
    連結:
  10. [45] Holger H. Hoos and Thomas Stutzle, “SATLIB: An Online Resource for Research on SAT,” Sat2000: highlights of satisfiability research in the year 2000, Ian Gent, Hans van Maaren, and Toby Walsh, Eds. Amsterdam, The Netherlands: IOS Press, 2000, pp.283-292, SATLIB is available online at www.satlib.org.
    連結:
  11. [3] Joao P. Marques Silva and Karem A. Sakallah, “GRASP - A New Search Algorithm for Satisfiability,” Proceedings of the 1996 IEEE/ACM International Conference on Computer-Aided Design, Los Alamitos, California, United States, pp.220-227, 1996.
  12. [5] Joao Marques-Silva, Ines Lynce, and Sharad Malik, “Conflict-Driven Clause Learning SAT Solvers,” Handbook of Satisfiability, Armin Biere et al., Eds.: IOS Press, 2009, ch. 4, pp.131-153.
  13. [6] Carla P. Gomes, Bart Selman, and Henry Kautz, “Boosting combinatorial search through randomization,” Proceedings of the 15th national/tenth conference on Artificial intelligence/Innovative applications of artificial intelligence, Madison, Wisconsin, United States, pp.431-437, 1998.
  14. [8] Armin Biere, “Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010,” Technical Report 10/1, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr, 69, 4040 Linz, Austria, 2010.
  15. [9] (2009, September) SAT 2009 competitive events booklet: preliminary version. [Online]. http://www.cril.univ-artois.fr/SAT09/solvers/booklet.pdf
  16. [10] Mate Soos. (2010, September) Homepage of Mate Soos. [Online]. http://www.msoos.org/creating-a-sat-solver-from-scratch
  17. [11] NVIDIA Corporation. (2011, May) CUDA C Programming Guide Version 4.0.
  18. [12] Gunnar Stalmarck, “A System for Determining Propositional Logic Theorems by Applying Values and Rules to Triplets that are Generated from a Formula,” Swedish Patent No. 467076 (1992), U.S. Patent No. 5276897 (1994), European Patent No. 0403454 (1995), 1992.
  19. [13] Gunnar Stalmarck, A Proof Theoretic Concept of Tautological Hardness, 1994, Unpublished manuscript.
  20. [15] Bart Selman, Hector Levesque, and David Mitchell, “A New Method for Solving Hard Satisfiability Problems,” Proceedings of the 10th National Conference on Artificial Intelligence, San Jose, California, United States, pp.440-446, 1992.
  21. [16] Bart Selman, Henry A. Kautz, and Bram Cohen, “Noise Strategies for Improving Local Search,” Proceedings of the 12th national conference on Artificial intelligence (vol. 1), Seattle, Washington, United States, pp.337-343, 1994.
  22. [17] (2009) The International SAT Competition 2009. [Online]. http://www.satcompetition.org/2009/
  23. [18] (2010) SAT-Race 2010. [Online]. http://baldur.iti.uka.de/sat-race-2010/
  24. [19] Youssef Hamadi, Said Jabbour, and Lakhdar Sais, “ManySat: solver description,” Technical Report, Microsoft Research, 2008.
  25. [21] Alex S. Fukunaga, “Massively parallel evolution of SAT heuristics,” IEEE Congress on Evolutionary Computation, 2009, Trondheim, Norway, pp.1478-1485, 2009.
  26. [22] Kanupriya Gulati, Paul Suganth, Sunil P. Khatri, Srinivas Patil, and Abhijit Jas, “FPGA-based hardware acceleration for Boolean satisfiability,” Journal of ACM Transactions on Design Automation of Electronic Systems (TODAES), vol.14, no.2, pp.1084-4309, April 2009.
  27. [23] Kanupriya Gulati and Sunil P. Khatri, “Boolean satisfiability on a graphics processor,” Proceedings of the 20th symposium on Great lakes symposium on VLSI, Providence, Rhode Island, USA, pp.123-126, 2010.
  28. [25] Joel Chavas, Cyril Furtlehner, Marc Mezard, and Riccardo Zecchina, “Survey-propagation decimation through distributed local computations,” Journal of Statistical Mechanics: Theory and Experiment, vol.2005, no.11, November 2005.
  29. [26] Niklas Een and Niklas Sorensson, “An Extensible SAT-solver,” 6th International Conference on Theory and Applications of Satisfiability Testing, Santa Margherita Ligure, Italy, vol.2919/2004 333-336, pp.502-518, 2003.
  30. [27] Quirin Meyer, Fabian Schonfeld, Marc Stamminger, and Rolf Wanka, “3-SAT on CUDA: Towards a Massively Parallel SAT Solver,” 2010 International Conference on High Performance Computing and Simulation (HPCS), Caen, France, pp.306-313, 2010.
  31. [28] Herve Deleau, Christophe Jaillet, and Michael Krajecki, “GPU4SAT: solving the SAT problem on GPU,” Proceedings of 9th International Workshop on State-of-the-Art in Scientific and Parallel Computing, Trondheim, Norway, 2008.
  32. [29] Google Incorporation. Google code. [Online]. http://code.google.com/
  33. [30] Stephen A. Cook, “The complexity of theorem-proving procedures,” Proceedings of the third annual ACM symposium on Theory of computing, Shaker Heights, Ohio, United States, pp.151-158, 1971.
  34. [31] Leonid Anatolievich Levin, “Universal'nyie perebornyie zadachi (Universal Sequential Search Problems, in Russian),” Problemy Peredachi Informatsii, vol.9, no.3, pp.115-116, 1973.
  35. [32] Antti E. J. Hyvarinen, Tommi Junttila, and Ilkka Niemela, “Incorporating Clause Learning in Grid-Based Randomized SAT Solving,” Journal on Satisfiability, Boolean Modeling and Computation, vol.6, pp.223-244, June 2009.
  36. [33] Kei Ohmura and Kazunori Ueda, “c-sat: A Parallel SAT Solver for Clusters,” Proceedings of the 12th International Conference on Theory and Applications of Satisfiability Testing, Swansea, United Kingdom, pp.524-537, 2009.
  37. [35] Leonardo Dagum and Ramesh Menon, “OpenMP: An Industry Standard API for Shared-Memory Programming,” Computational Science & Engineering, IEEE, vol.5, no.1, pp.46-55, January-March 1998.
  38. [36] NVIDIA Corporation. (2009, October) NVIDIA's Next Generation CUDA Compute Architecture: Fermi.
  39. [37] David H. Wolpert and Kagan Tumer, “An Introduction to Collective Intelligence,” Technical Report, Ames Research Center, Intelligent Systems Division, NASA, Moett Field, 1999.
  40. [38] Ramin Zabih and David McAllester, “A rearrangement search strategy for determining propositional satisfiability,” National Conference on Artificial Intelligence, pp.155-160, July 1988.
  41. [39] Joao P. Marques-Silva and Karem A. Sakallah, “Boolean Satisfiability in Electronic Design Automation,” Proceedings of the 37th Annual Design Automation Conference, Los Angeles, California, United States, pp.675-680, 2000.
  42. [40] Paul Beame, Henry Kautz, and Ashish Sabharwal, “Towards Understanding and Harnessing the Potential of Clause Learning,” Journal of Artificial Intelligence Research, vol.22, no.1, pp.319-351, July 2004.
  43. [41] Robert Tarjan, “Finding Dominators in Directed Graphs,” Society for Industrial and Applied Mathematics Journal on Computing, vol.3, no.1, pp.62-89, March 1974.
  44. [42] Joao P. Marques Silva and Karem A. Sakallah, “Dynamic search-space pruning techniques in path sensitization,” Proceedings of the 31st annual Design Automation Conference, San Diego, California, United States, pp.705-711, 1994.
  45. [44] Sharad Malik. (2004) Sharad Malik. [Online]. http://www.princeton.edu/~sharad/CMUSATSeminar.pdf
  46. [46] (2000, August) SATLIB - Benchmark Problems. [Online]. http://www.cs.ubc.ca/~hoos/SATLIB/benchm.html