期刊文献+

基于硬件模拟的SAT求解框架

A Hardware Framework of SAT Solver
下载PDF
导出
摘要 使用硬件方法求解SAT问题,采用现场可编程门阵列(FPGA)技术,针对大规模实际系统的CNF公式实例,定制化编译和转换为FPGA芯片,并完全依据FPGA硬件完成SAT满足性求解过程. In this paper, we customized the FPGA chip to fit the SAT problem,e, g. ,translating and compiling the large scale system,and then seccessfully solved the problem by FPGA autonomously.
出处 《微电子学与计算机》 CSCD 北大核心 2016年第9期124-127,共4页 Microelectronics & Computer
基金 国家自然科学基金(61402121 11371003 11461006) 广西自然科学基金(2013GXNSFAA019342 2012GXNSFGA060003) 广西高校科学技术研究项目(ZD2014044) 广西教育厅科研资助项目(201012MS274) 广西民族大学2015年研究生教育创新计划项目(gxun-chxs2015097)
  • 引文网络
  • 相关文献

参考文献6

  • 1张建民,沈胜宇,李思昆.可满足性求解技术研究[J].计算机工程与科学,2010(1):50-54. 被引量:4
  • 2黄文奇,金人超.求解SAT问题的拟物拟人算法—Solar[J].中国科学(E辑),1997,27(2):179-186. 被引量:23
  • 3J T D. Sousa, J P Marques-Silva, M Abramovici. A configware/software approach to SAT solving[C]// Proc Ninth IEEE Int'Symp Field-Programmable Cus- tom Computing Machines. California: IEEE, 2001 : 239- 298.
  • 4N A Reis, J T de Sousa.On implementing a eonfig- ware/software SAT solver[C] //Proc 10th IEEE Int' 1 Sympl Field-programmable Custom Computing Ma- chines. Napa, California: IEEE, 2002 : 282-283.
  • 5周进,赵希顺.基于硬件可编程逻辑(FPGA)的SAT算法的综述[J].电子世界,2012(6):61-63. 被引量:3
  • 6P Zhong, M Martonosi, P Ashar, et al. Using config- urable computing to accelerate boolean satisfiablitiy [J]. IEEE trans Computer-Aided Design of Integrated Circuits and Systems, 1999,18(6) .861-868.

二级参考文献36

  • 1Ivancic F, Yang Z, Ganai M K, et al. Efficient SAT-Based Bounded Model Checking for Software Verifications [J ]. Theoretical Computer Science,2008, 404(3):256-274.
  • 2Stephan P, Brayton R, Sangiovanni V A. Combinational Test Generation Using Satisfiabitity [J]. IEEE Trans on Computer-Aided Design of Integrated Circuits and Systems, 1996,15 : 1167-1176.
  • 3Kautz H, Selman B. Planning as Satisfiability[C]//Proc of the European Conf on Artificial Intelligence, 1992:359-363.
  • 4Davis M, Putnam H. A Computing Procedure for Quantification Theory[J]. Journal of the ACM, 1960,7(3):201-215.
  • 5Davis M, Logemann G, Loveland D. A Machine Program for Theorem Proving[J]. Communications of the ACM, 1962,5 (7) : 394-397.
  • 6Selman B, Kautz H, Cohen t3. Local Search Strategies for Satisfiability Testing[C]//Proc of th 2nd DIMACS Implementation Challenge, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, 1996:521-532.
  • 7Bryant R E. Graph-Based Algorithms for Boolean Function Manipulation[J]. IEEE Trans on Computers, 1986,35: 677- 691.
  • 8Prestwich S, Lynce I. Local Search for Unsatisfiability[C]// Proc of the 9th Int'l Conf on Theory and Applications of Satisfiability Testing, 2006 : 283-296.
  • 9Audemard G, Simon L. GUNSAT: A Greedy Local Search Algorithm for Unsatisfiability[C] //Proc of the 20th Int'l Joint Conf of Artificial Intelligence, 2007: 2256-2261.
  • 10Brinkmann R, Drechsler R. RTL-Datapath Verification Using Integer Linear Programming[C]//Proc of the 7th Asia and South Pacific Design Automation Conf, 2002:741-746.

共引文献27

;
使用帮助 返回顶部