期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息

基于硬件可编程逻辑(FPGA)的SAT算法的综述 被引量：3

下载PDF
导出
摘要 可满足性问题(简称SAT问题)作为第一个被证明的NP完全问题,是计算机科学的核心问题之一。本文系统总结了基于硬件可编程逻辑(FPGA---Field Programmable Gate Array)的SAT算法研究。将基于FPGA的SAT算法研究分为了实例型(instance-speci-ed solver)和应用型(application-speci-ed solver)两种类型。通过对各种方法的深入分析,指出了它们的优点和缺陷,进而提出未来研究的思路。
作者 周进 赵希顺
机构地区 中山大学逻辑与认知研究所
出处 《电子世界》 2012年第6期61-63,69,共4页 Electronics World
基金 国家自然科学基金资助项目(项目编号:60970040)
关键词 可编程逻辑 SAT算法 可满足性 FPGA
分类号 TN911.72 [电子电信—通信与信息系统]
  • 相关文献

参考文献13

  • 1M.Yokoo,T.Suyama,H.Sawada. Solving Satrsfiability problems Using Field Programmable Gate Arrays:First Results[A].1996.497-509.
  • 2P.Goel. An Implicit Enumeration Algonthm to Generate Tests for Combinatorial Logic Circuits[J].IEEE Transaction on Computer,1981,(03):215-222.
  • 3KcsturS,Davis,J.D,Williams,O. "BLAS Comparison on FPGA,CPU and GPU" VLSI (ISVLSI)[A].
  • 4N.A Reis,J.T.de Sousa. On Implementing a Configware/Software SAT Solver[A].2002.282-283.
  • 5B.Selman,H.Levesque,D.Mitchell. A New Method for Solving Hard Sausfiability Problems[A].1992.440-446.doi:10.1016/j.vaccine.2010.05.073.
  • 6S.A.Guccione. "Reconfigurable Computing at Xiltnx," keynote talk[A].2001.doi:10.1038/ajg.2009.624.
  • 7M Abramovici,D.Saab. Satisfiability on Reconfigurable Hardware[A].1997.448-456.
  • 8M.Davts,G.Logemann,D.Loveland. A Machine Program for Theorem Proving[J].Communications of the ACM,1962,(05):394-397.
  • 9L.M.Silva,K.A.Sakallah. GRASP:A Search Algorithm for Propositional Sausfiability[J].IEEE Transaction on Computer,1999,(05):506521.
  • 10J.de Sousa,J.P.Marques Silva,M.Abramovici. A Configware/Software Approach to SAT Solving[A].2001.doi:10.1016/j.jmb.2010.02.044.

同被引文献176

  • 1孙伟,马绍汉.分布式博弈树搜索算法[J].计算机学报,1995,18(1):39-45. 被引量：1
  • 2袁志斌,徐正权,王能超.软件模型检测中的抽象[J].计算机科学,2006,33(7):276-279. 被引量：5
  • 3文艳军,王戟,齐治昌.并发反应式系统的组合模型检验与组合精化检验[J].软件学报,2007,18(6):1270-1281. 被引量：17
  • 4Clarke E, Emerson E. Design and synathesis of synchronization skeletons using branching time temporal logic [C] // Procee- dings of Logic of Programs, 1981,5000(131) : 52-71.
  • 5Queille J, Sifakis J. Specification and verification of concurrent systems in CESAR[C]//Proceedings of the 5th Colloquium on International Symposium on Programming. LNCS 137, 1982: 337-351.
  • 6Clarke E, Filkorn T, Jha S. Exploiting symmetry in temporal logic model ehecking[C]//Courcoubetis C, ed, Proceedings of the 5th Int'l Conf. on Computer-Aided Verification. LNCS 697, 1993:450-461.
  • 7Emerson E, Sistla A. Symmetry and model checking [C~//Pro- ceedings of the 5th int'l Conf. on Computer-Aided Verification. LNCS 697,1993 : 105-131.
  • 8Norris I C, Dill D. Better verification through syrnmetry[J]. For- mal Methods in System Design, 1996,9 (1/2) : 41-75.
  • 9Sistla A, Godefroid P. Symmetry and reduced symmetry in mo- del checking[C]//CAV. LNCS 2102,2001 : 91-103.
  • 10Iosif R. Symmetry reduction criteria for software model checking [C] //Proceedings of SPIN Workshop. LNCS 2318,2002:22-41.

引证文献3

二级引证文献29

电子世界
2012年 第6期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部