臺灣博碩士論文加值系統

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

通用計算於圖形處理單元也在大量平行運算的領域之中興起。為了探討大量平行化布爾可滿足性解法器的概念，我們運用計算統一設備架構的平台，實現了名為「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.

口試委員會審定書 #
誌謝 i
中文摘要 ii
Abstract iii
Contents iv
List of Figures vii
List of Tables xi
Chapter 1 Introduction 1
Chapter 2 Previous Work 4
2.1 The Categories of SAT Solvers 4
2.2 Parallel SAT solvers 5
2.2.1 Plingeling and ManySAT 7
2.2.2 Decision Divergence and Learnt Clauses Exchange 8
2.3 SAT Solvers on CUDA 8
Chapter 3 Preliminaries 10
3.1 Boolean Satisfiability 10
3.1.1 Definitions 10
3.1.2 SAT Applications 14
3.2 Compute Unified Device Architecture (CUDA) 15
3.2.1 Hardware Architecture 15
3.2.2 Programming Model 16
Chapter 4 CUDASAT 24
4.1 Overview of CUDASAT 24
4.1.1 Massive Parallelization 24
4.1.2 GPGPU vs. CPU 24
4.1.3 CUDASAT: A Parallel SAT Solver on CUDA 26
4.2 Program Overview 28
4.3 Solver Phase 32
4.3.1 DPLL (Davis-Putnam-Logemann-Loveland) Algorithm 33
4.3.2 Boolean Constraint Propagation (BCP) 35
4.3.3 Two-Watched-Literal Scheme 37
4.3.4 Conflict Analysis 39
4.3.5 Clause Learning 41
4.3.6 The First Unique Implication Point (UIP) 42
4.3.7 Non-Chronological Back-Tracking 43
4.4 Shared Learnt Clauses 45
4.5 Memory Management 48
Chapter 5 Experimental Results 50
5.1 Description of Cases 50
5.2 Environment Setup 51
5.3 Experimental Results 52
5.3.1 Industrial SAT Problem: logistics.b 52
5.3.2 Comparison of Configurations: logistics.b 61
5.3.3 Discussion: logistics.b 62
5.3.4 Industrial UNSAT Problem: qg4-08 64
5.3.5 Comparison of Configurations: qg4-08 73
5.3.6 Discussion: qg4-08 74
5.3.7 Random SAT Problem: f150s 76
5.3.8 Comparison of Configurations: f150s 85
5.3.9 Discussion: f150s 86
5.3.10 Random UNSAT Problem: f100u 87
5.3.11 Comparison of Configurations: f100u 96
5.3.12 Discussion: f100u 97
Chapter 6 Conclusions and Future Work 98
Reference 99

[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.
[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.
[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.
[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.
[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.
[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.
[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.
[9](2009, September) SAT 2009 competitive events booklet: preliminary version. [Online]. http://www.cril.univ-artois.fr/SAT09/solvers/booklet.pdf

[10]Mate Soos. (2010, September) Homepage of Mate Soos. [Online]. http://www.msoos.org/creating-a-sat-solver-from-scratch

[11]NVIDIA Corporation. (2011, May) CUDA C Programming Guide Version 4.0.
[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.
[13]Gunnar Stalmarck, A Proof Theoretic Concept of Tautological Hardness, 1994, Unpublished manuscript.
[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.
[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.
[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.
[17](2009) The International SAT Competition 2009. [Online]. http://www.satcompetition.org/2009/

[18](2010) SAT-Race 2010. [Online]. http://baldur.iti.uka.de/sat-race-2010/

[19]Youssef Hamadi, Said Jabbour, and Lakhdar Sais, “ManySat: solver description,” Technical Report, Microsoft Research, 2008.
[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.
[21]Alex S. Fukunaga, “Massively parallel evolution of SAT heuristics,” IEEE Congress on Evolutionary Computation, 2009, Trondheim, Norway, pp.1478-1485, 2009.
[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.
[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.
[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.
[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.
[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.
[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.
[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.
[29]Google Incorporation. Google code. [Online]. http://code.google.com/

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

[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.
[36]NVIDIA Corporation. (2009, October) NVIDIA''s Next Generation CUDA Compute Architecture: Fermi.
[37]David H. Wolpert and Kagan Tumer, “An Introduction to Collective Intelligence,” Technical Report, Ames Research Center, Intelligent Systems Division, NASA, Moett Field, 1999.
[38]Ramin Zabih and David McAllester, “A rearrangement search strategy for determining propositional satisfiability,” National Conference on Artificial Intelligence, pp.155-160, July 1988.
[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.
[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.
[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.
[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.
[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.
[44]Sharad Malik. (2004) Sharad Malik. [Online]. http://www.princeton.edu/~sharad/CMUSATSeminar.pdf

[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.
[46](2000, August) SATLIB - Benchmark Problems. [Online]. http://www.cs.ubc.ca/~hoos/SATLIB/benchm.html