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

变量极小公式复杂性 被引量：1

原文传递
导出
摘要 基于逻辑公式的极小变量集合的需求,研究了变量极小等价(VME)和变量极小可满足(VMS)问题的理论性质.引入等价关键变量和可满足关键变量概念,证明它们的判定复杂性分别为NP-完全和DP-完全.通过等价关键变量和可满足关键变量,分别定义VME和VMS.证明了Unique-SATVMSVMESAT,其中Unique-SAT是具有唯一成真赋值的公式类.进一步证明VME是NP-完全,VMS属于DP且是coNP-难.
作者 陈振宇 徐宝文 丁德成
机构地区 南京大学计算机软件新技术国家重点实验室 南京大学软件学院 南京大学数学系
出处 《科学通报》 CAS CSCD 北大核心 2010年第12期1189-1193,共5页 Chinese Science Bulletin
基金 国家自然科学基金(批准号:60803007,90818027和10871091) 国家高技术研究发展计划(编号:2009AA01Z147) 国家重点基础研究发展计划(编号:2009CB320703)资助项目
关键词 极小不可满足 基本蕴含数 变量极小等价 变量极小可满足
分类号 TP301.6 [自动化与计算机技术—计算机系统结构]
  • 相关文献

参考文献18

二级参考文献33

  • 1许道云.不可满足公式的同态证明系统[J].软件学报,2005,16(3):336-345. 被引量：6
  • 2苏开乐,骆翔宇,吕关锋.符号化模型检测CTL[J].计算机学报,2005,28(11):1798-1806. 被引量：24
  • 3Ravi K,Somenzi F.Minimal assignments for bounded model checking.In:Jensen K,Podelski A,eds.Proc.of the 10th Conf.on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004).LNCS 2988,Heidelberg:Springer-Verlag,2004.31-45.
  • 4Jin HS,Ravi K,Somenzi F.Fate and free will in error traces.In:Katoen JP,Stevens P,eds.Proc.of the 8th Conf.on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2002).LNCS 2280,Heidelberg:Springer-Verlag,2002.445-459.
  • 5Clarke EM,Gupta A,Kukula JH,Shrichman O.SAT based abstraction-refinement using ILP and machine learning techniques.In:Brinksma E,Larsen KG,eds.Proc.of the 14th Int'l Conf.Computer Aided Verification (CAV 2002).LNCS 2404,Heidelberg:Springer-Verlag,2003.265-279.
  • 6Chauhan P,Clarke E,Kroening D.Using SAT based image computation for reachability analysis.Technical Report,CMU-CX-03-151,Pittsburgh:School of Computer Science,Carnegie Mellon University,2003.
  • 7Cimatti A,Clarke EM,Giunchiglia E,Giunchiglia F,Pistore M,Roveri M,Sebastiani R,Tacchella A.NuSMV 2:An open source tool for symbolic model checking.In:Brinksma E,Larsen KG,eds.Proc.of the 14th Int'l Conf.on Computer Aided Verification(CAV 2002).LNCS 2404,Heidelberg:Springer-Verlag,2002.359-364.
  • 8http://www.ee.vt.edu/～ha/cadtools/download.cgi
  • 9McMillan KL.Symbolic model checking:An approach to the state explosion problem[Ph.D.Thesis].Pittsburgh:Carnegie Mellon University,1992.
  • 10Biere A,Cimatti A,Clarke EM,Fujita M,Zhu YS.Symbolic model checking using SAT procedures instead of BDDs.In:Proc.of the 36th Conf.on Design Automation (DAC'99).New Orleans:ACM,1999.317-320.

共引文献30

同被引文献10

  • 1JONES J, HARROLD M. Test-suite reduction and prioritization for modified condition/decision eoverage[J]. IEEE Transactions on Software Engineering, 2003,29 (3): 195-209.
  • 2CHEN Z, CHEN T, XU B. A revisit of fault class hierarchies in general Boolean specifications[J]. ACM Transactions on Software Engineering and Methodology, 2011,20 (3) : 13.
  • 3WANG Z, CHEN Z, XU B. Fault class prioritization in Boolean expressions [C]//Proceedings of the 27th Annual ACM Symposium on Applied Computing. New York: ACM Press, 2012:1191-1196.
  • 4CHOUDHARY S, DUVALL J, JIN W, et al. Platform sup port for developing testing and analysis plugins[C]//Proeeed ings of the 1st Workshop on Developing Tools as Plugins.New York= ACM Press, 2011: 16-19.
  • 5MARIANI L, PASTORE F. Supporting plug-in mashes to ease tool integration[C]//Proceedings of the 1st Workshop on Developing Tools as Plug-ins. New York: ACM Press, 2011 : 1- 4.
  • 6YOO S, HARMAN M. Regression testing minimization, selection and prioritization: a survey[J]. Software Testing, Verification and Reliability,2012,22(2): 67-120.
  • 7LI Z, HARMAN M, HIERONS R. Search algorithms on for regression test ease prioritization[J]. IEEE Transactions on Software Engineering, 2007,33 (4) : 225-237.
  • 8MASRI W, PODGURSKI A, LEON D. An empirical study of test case filtering techniques based on exercising information flows[J]. IEEE Transactions on Software Engineering, 2007, 33(7) : 454-477.
  • 9ROTHERMEL G, UNTCH R, CHU C, et al. Test case prioritization., an empirical study[C]//Proceedings International Conference on Software Maintenance. Piscataway, NJ: IEEE Press, 1999 : 179-199.
  • 10YANG Q, LI J, WEISS D. A survey of coverage based tes ting tools[C]//Proceedings of the 2006 International Workshop on Automation of Software Test. New York: ACM Press,2006: 99-103.

引证文献1

科学通报
2010年 第12期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

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