布林可滿足性（SAT）問題是確定現有的賦值是否可以使命題公式被評估為真。許多技術問題，包括SoC驗證問題，已被證明能夠映射到SAT問題，因此許多電子設計自動化（EDA）領域的專家正在研究它們並獲得許多富有成效的結果。隨著EDA和人工智能技術的快速發展，我們現在看到SAT問題的規模越來越大。 SAT問題的大小確實會對計算資源構成挑戰，並且會佔用大量執行時間。這是因為布林約束傳播（BCP）最初是順序執行的。基於DPLL的SAT求解器在BCP過程中花費80-90％的CPU時間，並且在軟體SAT求解器中難以改進。

為了提高SAT求解器的性能，我們提出了一種新的硬體SAT求解器架構。該求解器可加速BCP過程並支持非按時間順序的回溯。該求解器支持並行操作，最多可執行511個變量的CNF問題大小，同時遍歷和評估多個子句並通過流水線結構同時檢測衝突。我們的硬體架構中有一個3級流水線，它可以執行8個子句並同時檢測衝突。實驗結果表明，我們提出的求解器比以前的算法實現了1.35倍和高達453倍的加速，並且它代表了我們提出的加速BCP過程的方法是有效的。

Boolean satisfiability (SAT) problem is to determine whether existing an assignment can make propositional formula be evaluated as true. Many technology issues, including SoC verification problems, have been proved to be able to map to SAT problem, and thus lots of the experts of electronics design automation (EDA) region are working on them and deriving many fruitful results. With rapid development in EDA and artificial intelligence technology, we now see the size of SAT problems is getting larger and larger. The very large size of SAT problems does challenge the computation resource and consume lots of execution time. It is because that Boolean Constraint Propagation (BCP) is originally executed sequentially. DPLL-based SAT solvers spend 80-90\% of CPU time on BCP process and it is hard to be improved in software SAT solver.

To improve the performance of SAT solver, we proposed a new hardware SAT solver architecture. This solver accelerates BCP process and supports non-chronological backtracking. This solver supports parallelism with executing up to the CNF problems size of 512 variables, while traverses and evaluates several clauses and detect conflict simultaneously by pipelining structure. There is a 3 stage-pipeline in our hardware architecture, and it can execute 8 clauses and detect conflict at the same time. Experimental result shows that our proposed solver achieves 1.35x and up to 453x speedup than previous works, and it represents that the way which our proposed to accelerate BCP process is efficient.

[1] SATLIB Benchmark Suite. https://www.cs.ubc.ca/ hoos/SATLIB/benchm.html.
[2] Jean-Loup Baer. Microprocessor architecture: from simple pipelines to chip multiprocessors. Cambridge University Press, 2009.
[3] John D Davis, Zhangxi Tan, Fang Yu, and Lintao Zhang. A practical reconfigurable hardware accelerator for boolean satisfiability solvers. In Design Automation Conference, 2008. DAC 2008. 45th ACM/IEEE, pages 780–785. IEEE, 2008.
[4] Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem-proving. Communications of the ACM, 5(7):394–397, 1962.
[5] Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the ACM (JACM), 7(3):201–215, 1960.
[6] Niklas Een. Minisat: A sat solver with conflict-clause minimization. In Proc. SAT-05: 8th Int. Conf. on Theory and Applications of Satisfiability Testing, pages 502–518, 2005.
[7] Niklas Eén and Armin Biere. Effective preprocessing in sat through variable and clause elimination. In International conference on theory and applications of satisfiability testing, pages 61–75. Springer, 2005.
[8] Niklas Eén and Niklas Sörensson. An extensible sat-solver. In International conference on theory and applications of satisfiability testing, pages 502–518. Springer, 2003.
[9] Kanupriya Gulati, Mandar Waghmode, Sunil P Khatri, and Weiping Shi. Efficient, scalable hardware engine for boolean satisfiability and unsatisfiable core extraction. IET Computers & Digital Techniques, 2(3):214–229, 2008.
[10] Kenji Kanazawa and Tsutomu Maruyama. An approach for solving large sat problems on fpga. ACM Transactions on Reconfigurable Technology and Systems (TRETS), 4(1):10, 2010.
[11] Alan Mishchenko, Satrajit Chatterjee, Robert Brayton, and Niklas Een. Improvements to combinational equivalence checking. In Proceedings of the 2006 IEEE/ACM international conference on Computer-aided design, pages 836–843. ACM, 2006.
[12] Matthew W Moskewicz, Conor F Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient sat solver. In Proceedings of the 38th annual Design Automation Conference, pages 530–535. ACM, 2001.
[13] Richard Ostrowski, Éric Grégoire, Bertrand Mazure, and Lakhdar Sais. Recovering and exploiting structural knowledge from cnf formulas. In International Conference on Principles and Practice of Constraint Programming, pages 185–199. Springer, 2002.
[14] Mona Safar, M Watheq El-Kharashi, and Ashraf Salem. Fpga-based sat solver. In Electrical and Computer Engineering, 2006. CCECE’06. Canadian Conference on, pages 1901–1904. IEEE, 2006.
[15] Mona Safar, M Watheq El-Kharashi, Mohamed Shalan, and Ashraf Salem. A reconfigurable, pipelined, conflict directed jumping search sat solver. In Design, Automation & Test in Europe Conference & Exhibition (DATE), 2011, pages 1–6. IEEE, 2011.
[16] Mona Safar, Mohamed Shalan, M Watheq El-Kharashi, and Ashraf Salem. A shift register based clause evaluator for reconfigurable sat solver. In Design, Automation & Test in Europe Conference & Exhibition, 2007. DATE’07, pages 1–6. IEEE, 2007.
[17] João P Marques Silva and Karem A Sakallah. Grasp—a new search algorithm for satisfiability. In The Best of ICCAD, pages 73–89. Springer, 2003.
[18] Iouliia Skliarova and Antonio de Brito Ferrari. A software/reconfigurable hardware sat solver. IEEE Transactions on Very Large Scale Integration (VLSI) Systems, 12(4):408–419, 2004.
[19] 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.
[20] Grigori Tseitin. On the complexity of derivation in propositional calculus. Studies in constructive mathematics and mathematical logic, pages 115–125, 1968.