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

Abstract

解決布爾可滿足性問題在理論與工業應用上，扮演著極為關鍵角色。十五年來，布爾可滿足性解法器有著長足的進展，得以解決相當大型的問題。為了進一步解決更大型、更困難的布爾可滿足性問題，平行化布爾可滿足性解法器於近年來受到相當關注。最近幾年的國際布爾可滿足性解法器比賽之中，最佳的四至八線程平行化布爾可滿足性解法器的成績勝過最佳單線程布爾可滿足性解法器。 通用計算於圖形處理單元也在大量平行運算的領域之中興起。為了探討大量平行化布爾可滿足性解法器的概念，我們運用計算統一設備架構的平台，實現了名為「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.