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

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

林拱民(Kung-Ming Lin)

指導教授 ： 黃鐘揚

國立臺灣大學/電機資訊學院/電子工程學研究所/碩士(2011年)

https://doi.org/10.6342/NTU.2011.01461

摘要

解決布爾可滿足性問題在理論與工業應用上，扮演著極為關鍵角色。十五年來，布爾可滿足性解法器有著長足的進展，得以解決相當大型的問題。為了進一步解決更大型、更困難的布爾可滿足性問題，平行化布爾可滿足性解法器於近年來受到相當關注。最近幾年的國際布爾可滿足性解法器比賽之中，最佳的四至八線程平行化布爾可滿足性解法器的成績勝過最佳單線程布爾可滿足性解法器。

通用計算於圖形處理單元也在大量平行運算的領域之中興起。為了探討大量平行化布爾可滿足性解法器的概念，我們運用計算統一設備架構的平台，實現了名為「CUDASAT」的子句分享平行化、衝突驅使子句學習、戴維斯-普特南-羅格曼-羅夫蘭演算法布爾可滿足性解法器。

根據我們瞭解，目前尚未有類似CUDASAT的程式。實驗結果顯示，提昇平行解法器的數量時，平均每個解法器於搜尋上所用的步驟有著明顯下降的趨勢。CUDASAT的效能無法與現今最好的平行化布爾可滿足性解法器相比。它是作為發展大量平行化、低成本、替代性布爾可滿足性解法器的原型。

關鍵字

布爾可滿足性問題 ； 可滿足性解法器 ； 平行運算 ； 衝突驅使子句學習 ； 戴維斯-普特南-羅格曼-羅夫蘭 ； 通用計算於圖形處理單元 ； 計算統一設備架構

並列摘要

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.

並列關鍵字

Boolean satisfiability problem ； satisfiability solver ； parallel computing ； SAT ； CDCL ； DPLL ； GPGPU ； CUDA

參考文獻

[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.

[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.

[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.

[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] 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.