MA Kefan, XIAO Liquan, ZHANG Jianmin, LI Tiejun. Accelerating an FPGA-Based SAT Solver by Software and Hardware Co-design[J]. Chinese Journal of Electronics, 2019, 28(5): 953-961. doi: 10.1049/cje.2019.06.015
Citation: MA Kefan, XIAO Liquan, ZHANG Jianmin, LI Tiejun. Accelerating an FPGA-Based SAT Solver by Software and Hardware Co-design[J]. Chinese Journal of Electronics, 2019, 28(5): 953-961. doi: 10.1049/cje.2019.06.015

Accelerating an FPGA-Based SAT Solver by Software and Hardware Co-design

doi: 10.1049/cje.2019.06.015
Funds:  This work is supported by the National Major Scientific Research Program (No.2016YFB0200203) and the National Natural Science Foundation of China (No.61103083, No.61133007).
  • Received Date: 2018-02-05
  • Rev Recd Date: 2018-09-17
  • Publish Date: 2019-09-10
  • The Boolean Satisfiability (SAT) problem is the key problem in computer theory and application. Field-programmable gate array (FPGA) has been addressed frequently to accelerate the SAT solving process in the last few years owing to its parallelism and flexibility. We have proposed a novel SAT solver based on an improved local search algorithm on the reconfigurable hardware platform. The new software preprocessing procedure and hardware architecture are involved to solve large-scale SAT problems instances. As compared with the past solvers, the proposed solver has the following advantages:the preprocessing technology can strongly improve the efficiency of solver; the strategy of strengthening the variable selection can avoid the same variable flipped continuously and repeatedly. It reduces the possibility of search falling into local minima. The experimental results indicate that the solver can solve problems of up to 32K variables/128K clauses without off-chip memory banks, and has better performance than previous works.
  • loading
  • 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.
    Mona Safar, M. Watheq El-Kharashi, Mohamed Shalan, et al., "A reconfigurable, pipelined, conflict directed jumping search SAT solver", In Design, Automation and Test in Europe, IEEE Proceedings, pp.978-981, 2011.
    Kenji Kanazawa and Tsutomu Maruyama, "An approach for solving large SAT problems on FPGA", Trans. ACM TRETS Vol.4, No.1, Article No.10, 2010.
    Kenji Kanazawa and Tsutomu Maruyama, "An FPGA solver for large SAT problems", In Proceedings of the International Conference on Field Programmable Logic and Applications (FPL' 07), pp.243-258, 2007.
    Kenji Kanazawa and Tsutomu Maruyama, "Solving SATencoded formal verification problems on SoC based on a WSAT algorithm with a new heuristic for hardware acceleration", International Symposium on Embedded Multicore/Manycore System-on-Chip, pp.101-106, 2013.
    Kenji Kanazawa and Tsutomu Maruyama, "FPGA acceleration of SAT/Max-SAT solving using variable-way cache", 24th International Conference on Field Programmable Logic and Applications, pp.1-4, 2014.
    Teodor Ivan and El Mostapha Aboulhamid, "An efficient hardware implementation of a SAT problem solver on FPGA", Euromicro Conf. on Digital System Design, pp.209-216, 2013.
    Leopold Haller and Satnam Singh, "Relieving capacity limits on FPGA-based SAT-solvers", In Formal Methods in Computer-aided Design, IEEE, pp.217-220, 2013.
    Jason Thong and Nicola Nicolic, "FPGA acceleration of enhanced boolean constraint propagation for SAT solvers", IEEE/ACM International Conference on Computer-aided Design, IEEE, pp.234-241, 2013.
    M. Davis, M. Logemann, and D. Loveland, "A machine program for theorem-proving", Communications of the ACM 5. pp.394-397, 1962.
    Zhang Jianmin, Shen Shengyu and Li Sikun, "An unsatisfiable subformulae extraction algorithm base on refutation proof and local search", Chinese Journal of Computer, Vol.37, No.11, pp.2262-2267, 2014. (in Chinese)
    Chen Yangzhi, "Research on genetic algorithm-based SAT problem solving", Master's Thesis, Harbin Engineering University, 2014. (in Chinese)
    N. Een and A. Biere, "Effective preprocessing in SAT through variable and clause elimination", International Conference on Theory and Applications of Satisfiability Testing, Springer, pp.61-75, 2005.
    Mcallester D A, Selman B, and Kautz H A, "Evidence for invariants in local search", National Conference on Artificial Intelligence, pp.321-326, 1997.
    A. Balint and U. Schoning, "Choosing probability distributions for stochastic local search and the role of make versus break", International Conference on Theory and Applications of Satisfiability Testing, pp.16-29, 2012.
    Dimitris Achlioptas, "Lower bounds for random 3-SAT via differential equations", Theoretical Computer Science, Vol.265, No.1, pp.159-185, 2001.
    Olivier Dubois, Yacine Boufkhad, and Jacques Mandler, "Typical random 3-sat formulae and the satisfiability threshold", Proceedings of Symposium on Discrete Algorithms, pp.126-127, 2000.
    J. M. Crawford and L. D. Auton, "Experimental results on the crossover point in satisfiability", Proc. of the 11th AAAI'93, Menlo Park, 1993.
    Xu Ke and Li Wei, "The SAT phase transition", Science in China(Series E), Vol.42, No.5, pp.494-501, 1999. (in Chinese)
    Yang Jinji and Su Kaile, "Improvement of local research in SAT problem", Journal of Computer Research and Development, Vol.42, No.1, pp.60-65, 2005.
    Yousef K, Mohammad B, Ayoub A, et al., "A survey of the satisfiability-problems solving algorithms", International Journal of Advanced Intelligence Paradigms, Vol.5, No.3, pp.233-256, 2013.
    "WalkSAT Version 51", https://github.com/tonyling/research-sat-solvers/,2019-3-18.
    "SATLIB benchmark problems", https://www.cs.ubc.ca/hoos/SATLIB/benchm.html/,2019-5-18.
    "SAT competition", http://www.satcompetition.org/,2019-1-21.
    A.A. Sohanghpurwala, M.W. Hassan and P. Athanas, "Hardware accelerated SAT solvers-A survey", Journal of Parallel and Distributed Computing, Vol.106, No.1, pp.170-184, 2017.
    Sohanghpurwala, Ali Asgar and P. Athanas, "An effective probability distribution SAT solver on reconfigurable hardware", International Conference on Reconfigurable Computing and FPGAs, IEEE, pp.1-6, 2017.
  • 加载中

Catalog

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

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

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

    Article Metrics

    Article views (198) PDF downloads(267) Cited by()
    Proportional views
    Related

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return