臺灣博碩士論文加值系統

決定一個布林函式是否能夠找到一組解帶入使布林函式的結果為真，這就是布林可滿足性問題。布林可滿足性問題被廣泛應用在電子自動化設計領域，包含電路合成，以及正規驗證等等。針對布林可滿足性問題的解法，一般分為完整演算法以及不完整演算法兩類。完整演算法是一個探索整個解空間的方法，可以證明問題是否有解;而不完整演算法是使用基於區域搜索的演算法，不記憶探索過的空間，所以無法證明問題是否有解，但是如果問題是有解的，則其有很大的機率能夠在很短的時間內找到一組解。
在電路驗證上會遇到資源不足的情況，電路設計越來越複雜時，完整演算法會遭遇搜索狀態空間爆炸的問題，導致搜索效率差的情況。
使用不完整演算法雖然沒辦法找完整個解空間，但是在短時間內可以找到比較多的解，且對於完整演算法不善於探索驗證深度比較深的地方
，透過不完整演算法的特性有機會能夠快速探索。

傳統的不完整演算法只從不滿足條件裡面選取變數做翻轉運算，而本篇論文則提出一個在不完整演算法裡面加入從出現在布林可滿足性問題的全域範圍裡面出現的變數翻轉的方法，由實驗數據證實使用這種方式可以讓不完整演算法的總翻轉次數減少，並且這種特別的翻轉運算比一般從不滿足條件選擇變數的翻轉運算更快，本篇論文亦將不完整演算法實作在現場可程式化邏輯陣列上，相較於過去的研究，我們平均加速了2.06倍的時間。

Determining whether a boolean formula can be find a set of solutions to bring the results of the boolean formula to true is boolean satisfiability(SAT) problem.
SAT problem is widely used in the field of electronic automation design(EDA), including circuit synthesis, and formal verification and so on. SAT algorithm is generally divided into two types: complete algorithm and incomplete algorithm.
Complete algorithm is a way to explore the entire solution space. It can prove whether the problem has a solution. Incomplete algorithm uses local search method
, which doesn't memorize the space that has been explored, so it cannot prove whether the problem has a solution, but if the problem is solved, it has a great chance of finding a set of solutions to be in a short time. In the case of circuit verification, you will encounter insufficient resources. When the circuit design becomes more and more complicated, complete algorithm will encounter the problem of explosion of the search state space, resulting in poor search efficiency. The disadvantage of using incomplete algorithm is no way to find a complete solution space, but it can find more solutions in a short time.
Complete algorithm is not good at exploring deep verification depth.
There are opportunities to explore quickly through the characteristics of incomplete algorithm.

Traditionally, incomplete algorithm only selects variables from the unsatisfied clause to do the flip operation.
However, this paper proposes a method of adding
the flip of the variable from the global scope of the SAT problem in the incomplete algorithm.
It is possible to reduce the total number of flips of the incomplete algorithm from experimental result, and this special flip operation is faster than the flip operation from unsatisfied clause.
This paper implements incomplete algorithms on the field programmable logic array(FPGA).
Compared to the previous work, we have accelerated the average time by 2.06 times.

目錄
摘要i
Abstract ii
英文延伸摘要iv
誌謝ix
目錄x
表格xii
圖片xiii
第一章緒論 1
1.1 SAT 問題 1
1.2 名詞介紹 1
1.3 電路驗證 3
1.4 SAT 演算法 5
1.4.1 完整演算法 6
1.4.2 不完整演算法 8
1.5 研究動機與論文貢獻 9
1.6 論文組織 10
第二章文獻探討 11
2.1 WalkSAT algorithm 11
2.2 Hardware SAT solver 12
2.2.1 Complete algorithm 14
2.2.2 軟硬體混合SAT solver 14
2.2.3 Incomplete algorithm 14
第三章研究方法 16
3.1 研究動機 16
3.2 全域式翻轉(Global flip) 17
3.3 演算法與硬體流程 18
3.4 硬體資料表示法 23
3.5 系統架構 25
3.6 系統前端驗證 40
第四章實驗結果 48
4.1 系統規格 48
4.2 Variable 初始化探討 50
4.3 機率對解決SAT 問題的影響 52
4.4 General flip 和Global flip 的比較 55
4.5 數據比較 58
第五章結論 62
5.1 未來展望 62
References 63

[1] 2018 sat competition http://sat2018.forsyte.tuwien.ac.at/.
[2] Mdpi. https://www.mdpi.com.
[3] Satlib https://www.cs.ubc.ca/ hoos/satlib/benchm.html.
[4] Martin Davis, George Logemann, and Donald Loveland. A machine program for
theorem-proving. Communications of the ACM, 5(7):394–397, 1962.
[5] Rina Dechter and Daniel Frost. Backjump-based backtracking for constraint satisfaction
problems. Artificial Intelligence, 136(2):147–188, 2002.
[6] Matti Järvisalo, Daniel Le Berre, and Olivier Roussel. 2011 sat competition
https://www.satcompetition.org/2011.
[7] Kenji Kanazawa and Tsutomu Maruyama. An fpga solver for wsat algorithms. In
International Conference on Field Programmable Logic and Applications, 2005.,
pages 83–88. IEEE, 2005.
[8] Kenji Kanazawa and Tsutomu Maruyama. An fpga solver for large sat problems.
In 2006 International Conference on Field Programmable Logic and Applications,
pages 1–6. IEEE, 2006.
[9] Kefan Ma, Liquan Xiao, and Jianmin Zhang. An effective fpga solver on probability
distribution and preprocessing. Electronics, 8(3):333, 2019.
[10] David McAllester, Bart Selman, and Henry Kautz. Evidence for invariants in
local search. In AAAI/IAAI, pages 321–326. Rhode Island, USA, 1997.
[11] Mona Safar, M Watheq El-Kharashi, Mohamed Shalan, and Ashraf Salem. A
reconfigurable, pipelined, conflict directed jumping search sat solver. In 2011
Design, Automation ＆ Test in Europe, pages 1–6. IEEE, 2011.
[12] Bart Selman, Henry A Kautz, and Bram Cohen. Noise strategies for improving
local search. In AAAI, volume 94, pages 337–343, 1994.
[13] Niklas Sorensson and Niklas Een. Minisat v1. 13-a sat solver with conflict-clause
minimization. SAT, 2005(53):1–2, 2005.
[14] Jason Thong and Nicola Nicolici. Fpga acceleration of enhanced boolean constraint
propagation for sat solvers. In Proceedings of the International Conference
on Computer-Aided Design, pages 234–241. IEEE Press, 2013.
[15] Grigori S Tseitin. On the complexity of derivation in propositional calculus. In
Automation of reasoning, pages 466–483. Springer, 1983.
[16] Lintao Zhang and Sharad Malik. The quest for efficient boolean satisfiability
solvers. In International Conference on Computer Aided Verification, pages 17–
36. Springer, 2002.