Volume 30 Issue 6
Nov.  2021
Turn off MathJax
Article Contents
LI Tiejun, MA Kefan, ZHANG Jianmin. An Parallel FPGA SAT Solver Based on Multi-Thread and Pipeline[J]. Chinese Journal of Electronics, 2021, 30(6): 1008-1016. doi: 10.1049/cje.2021.08.001
Citation: LI Tiejun, MA Kefan, ZHANG Jianmin. An Parallel FPGA SAT Solver Based on Multi-Thread and Pipeline[J]. Chinese Journal of Electronics, 2021, 30(6): 1008-1016. doi: 10.1049/cje.2021.08.001

An Parallel FPGA SAT Solver Based on Multi-Thread and Pipeline

doi: 10.1049/cje.2021.08.001

This work is supported by the National Key Research and Development Program of China (No.2018YFB0204301) and the National Natural Science Foundation of China (No.62072464, No.U19A2062).

  • Received Date: 2020-06-15
  • Rev Recd Date: 2021-07-02
  • Available Online: 2021-09-23
  • Publish Date: 2021-11-05
  • The Boolean Satisfiability (SAT) problem is the key problem in computer theory and application. A parallel multi-thread SAT solver named pprobSAT+ on a configurable hardware is proposed. In the algorithm, multithreads are executed simultaneously to hide the circuit stagnate. In order to improve the working frequency and throughput of the SAT solver, the deep pipeline strategy is adopted. When all data stored in block random access memory of the field programmable gate array, the solver can achieve maximum performance. If partial data are stored in the external memory, the size of the problem instances the SAT solver can be greatly improved. The experimental results show that the speedup of three-thread SAT solver is approximately 2.4 times with single thread, and shows that the pprobSAT+ have achieved substantial improvement while a solution is found.
  • loading
  • Bhattacharya B B, "ATPG binning and SAT-based approach to hardware trojan detection for safety-critical systems", 12th International Conference on Network and System Security, Hong Kong, China, pp.391-397, 2018.
    Ganesh V, "SAT and SMT Solvers:A foundational perspective", Engineering Secure and Dependable Software Systems, Vol.53, No.29, pp.29-60, 2019.
    Hülle R, Fier P and Schmidt J, "PBO-based fault selection for compact test generation", 7th Prague Embedded Systems Workshop, https://pesw.fit.cvut.cz/2019/index.php?page=Program,2019-6-27
    Zheng Y, Hsiao M S and Huang C, "SAT-based equivalence checking of threshold logic designs for nanotechnologies", Proceedings of the 18th ACM Great Lakes Symposium on VLSI, pp.225-230, 2008.
    Eibach T, Pilz E and Völkel G, "Attacking Bivium using SAT solvers", International Conference on Theory and Applications of Satisfiability Testing, pp.63-76, 2008.
    Tadesse D, Sheffield D, Lenge E, et al., "Accurate timing analysis using SAT and pattern-dependent delay models", Proceedings of the Conference on Design, Automation and Test in Europe, pp.1018-1023, 2007.
    I. Skliarova and A. B. Ferrari, "Reconfigurable hard-ware SAT solver:A survey of systems", IEEE Transaction on Computers, Vol.53, No.11, pp.1449-1461, 2004.
    Balint A, Belov A and Järvisalo M, "Overview and analysis of the SAT Challenge 2012 solver competition", Artificial Intelligence, pp.120-155, 2015.
    Ali Asgar Sohanghpurwala, Mohamed W Hassan and Peter Athanas, "Hardware accelerated SAT solvers-A survey", Journal of Parallel and Distributed Computing, Vol.106, pp.170-184, 2016.
    Safar, M., El-Kharashi, M.W., Shalan, M., et al., "A reconfigurable, pipelined, conflict directed jumping search SAT solver", Proceedings of the 2011 Design, Automation & Test in Europe, Grenoble, France, pp.14-18, 2011.
    Kanazawa, K. and Maruyama, T, "An approach for solving large SAT problems on FPGA", ACM Trans. Reconfigurable Technol. Syst., DOI:10.1145/1857927.1857937, 2010.
    Kanazawa, K. and Maruyama, T, "An FPGA solver for large SAT problems", Proceedings of the 2006 International Conference on Field Programmable Logic and Applications (FPL'06), Madrid, Spain, pp.28-30, 2006.
    Kanazawa, K. and Maruyama, T, "Solving SAT-encoded formal verification problems on SoC based on a WSAT algorithm with a new heuristic for hardware acceleration", Proceedings of the 2013 IEEE 7th International Symposium on Embedded Multicore Socs (MCSoC), Tokyo, Japan, pp.26-28, 2013.
    Kanazawa, K. and Maruyama, T, "FPGA acceleration of SAT/Max-SAT solving using variable-way cache", Proceedings of the 2014 24th International Conference on Field Programmable Logic and Applications (FPL), Munich, Germany, pp.2-4, 2014.
    Ivan, T. and Aboulhamid, E.M, "An efficient hardware implementation of a SAT problem solver on FPGA", Proceedings of the 2013 Euromicro Conference on Digital System Design (DSD), Los Alamitos, CA, USA, pp.4-6, 2013.
    Haller, L. and Singh, S, "Relieving capacity limits on FPGAbased SAT-solvers", Proceedings of the Formal Methods in Computer-Aided Design (FMCAD), Lugano, Switzerland, pp.20-23, 2010.
    Thong, J. and Nicolici, N, "FPGA acceleration of enhanced boolean constraint propagation for SAT solvers", Proceedings of the International Conference on Computer-Aided Design, San Jose, CA, USA, pp.18-21, 2013.
    Sohanghpurwala, A.A. and Athanas, P, "An effective probability distribution SAT solver on reconfigurable hardware", Proceedings of the 2016 International Conference on ReConFigurable Computing and FPGAs (ReConFig), Cancun, Mexico, pp.1-6, 2016.
    Quirin Meyer and Fabian Schönfeld, Marc Stamminger, et al., "3-SAT on cuda:Towards a massively parallel SAT solver", 2010 International Conference on High Performance Computing & Simulation, IEEE, pp.306-313, 2010.
    Duc Nghia Pham, Thach-Thao Duong and Abdul Sattar, "Trap avoidance in local search using pseudo-conflict learning", Twenty-Sixth AAAI Conference on Artificial Intelligence, https://dl.acm.org/doi/10.5555/2900728.2900806,2012-7-22.
    Suthep Nimnon, Marong Phadoongsidhi and N Utamaphethai, "Parallelization of stochastic algorithm for Boolean satisfiability on gpgpu architecture", 2012 9th International Conference on Electrical Engineering/Electronics, Computer, Telecommunications and Information Technology, IEEE, pp.1-4, 2012.
    Taeill Yoo, Sangpil Kim, Yongjin Yeom, et al., "A study of the parallelization of hybrid SAT solver using CUDA", Information Security and Assurance 2014, DOI:10.14257/astl.2014.48.04, 2014.
    Heng Liu, Wendy MacCaully and Xu Wang, "An efficient SAT solving algorithm using pseudo-conflict learning and heterogeneous computing", 2015 Third International Symposium on Computing and Networking (CANDAR), IEEE, pp.127-132, 2015.
    Kefan Ma, Liquan Xiao and Jianmin Zhang, "An effective fpga solver on probability distribution and preprocessing", Electronics, Vol.8, No.3, pp.333-339, 2019.
    Kefan Ma, Liquan Xiao, Jianmin Zhang, et al., "Accelerating an FPGA-based SAT solver by software and hardware co-design", Chinese Journal of Electronics, Vol.28, No.5, pp.953-961, 2019.
    Zhang, J., Shen, S. and Li, S, "An unsatisfiable subformulae extraction algorithm based on refutation proof and local search", Chin. J. Comput, Vol.37, pp.2262-2267, 2013.
    Mohammed, S.M.Z., Khader, A.T., Al-Betar and M.A, "3-SAT using island-based genetic algorithm", IEEJ Trans. Electron. Inf. Syst, Vol.136, No.12, pp.1694-1698, 2016.
    Marques-Silva, J, "Algebraic simplification techniques for propositional satisfiability", Proceedings of the International Conference on Principles and Practice of Constraint Programming, Singapore, pp.537-542, 2000.
    SAT, "The International SAT Competition Web Page:Feb 29, 2020", http://www.satcompetition.org,2020-2-29.
  • 加载中


    通讯作者: 陈斌, bchen63@163.com
    • 1. 

      沈阳化工大学材料科学与工程学院 沈阳 110142

    1. 本站搜索
    2. 百度学术搜索
    3. 万方数据库搜索
    4. CNKI搜索

    Article Metrics

    Article views (184) PDF downloads(48) Cited by()
    Proportional views


    DownLoad:  Full-Size Img  PowerPoint