| 
  中国学术期刊网络出版总库
  关闭
SMT求解技术简述  
   推荐 CAJ下载 PDF下载
【英文篇名】 Brief Introduction to SMT Solving
【下载频次】 ★★★★★
【作者】 金继伟; 马菲菲; 张健;
【英文作者】 JIN Jiwei; MA Feifei; ZHANG Jian; Institute of Software; Chinese Academy of Sciences;
【作者单位】 中国科学院软件研究所;
【文献出处】 计算机科学与探索 , Journal of Frontiers of Computer Science and Technology, 编辑部邮箱 2015年 07期  
期刊荣誉：中文核心期刊要目总览  ASPT来源刊  CJFD收录刊
【中文关键词】 可满足性模理论(SMT); DPLL(T); 求解器;
【英文关键词】 satisfiability modulo theories(SMT); DPLL(T); solver;
【摘要】 SMT问题是在特定理论下判定一阶逻辑公式可满足性问题。它在很多领域,尤其是形式验证、程序分析、软件测试等领域,都有重要的应用。介绍了SMT问题的基本概念、相关定义以及目前的主流理论。近年来出现了很多提高SMT求解效率的技术,着重介绍并分析了这些技术,包括积极类算法、惰性算法及其优化技术等。介绍了目前的主流求解器和它们各自的特点,包括Z3、Yices、CVC3/CVC4等。对SMT求解技术的前景进行了展望,量词的处理、优化问题和解空间大小的计算等尤其值得关注。
【英文摘要】 SMT is the problem of deciding the satisfiability of a first order formula with respect to some theory formulas.It is being recognized as increasingly important due to its applications in different communities, in particular in formal verification, program analysis and software testing. This paper provides a brief overview of SMT and its theories.Then this paper introduces some approaches aiming to improve the efficiency of SMT solving, including eager and lazy approaches and optimum technique which have be...
【基金】 国家自然科学基金~~
【更新日期】 2015-07-27
【分类号】 TP301.6
【正文快照】 1引言SAT(satisfiability)问题指的是命题逻辑公式的可满足性问题。随着研究的深入,人们发现SAT在表达能力上有很大的局限性,许多应用用SAT进行编码并不是很明智的选择,它们需要比SAT更强的表达方式。在这种形势下,将SAT问题扩展为SMT,经过扩展,SMT能比SAT更好地表达一些人工智

xxx
【读者推荐文章】中国期刊全文数据库 中国博士学位论文全文数据库 中国优秀硕士学位论文全文数据库
【相似文献】
中国期刊全文数据库
中国优秀硕士学位论文全文数据库
中国博士学位论文全文数据库
中国重要会议论文全文数据库
中国重要报纸全文数据库
中国学术期刊网络出版总库
点击下列相关研究机构和相关文献作者，可以直接查到这些机构和作者被《中国知识资源总库》收录的其它文献，使您全面了解该机构和该作者的研究动态和历史。
【文献分类导航】从导航的最底层可以看到与本文研究领域相同的文献，从上层导航可以浏览更多相关领域的文献。

工业技术
　 自动化技术、计算机技术
　　 计算技术、计算机技术
　　　 一般性问题
　　　　 理论、方法
　　　　　 算法理论
  
 
  CNKI系列数据库编辑出版及版权所有：中国学术期刊(光盘版)电子杂志社
中国知网技术服务及网站系统软件版权所有：清华同方知网(北京)技术有限公司
其它数据库版权所有：各数据库编辑出版单位（见各库版权信息）
京ICP证040431号    互联网出版许可证 新出网证（京）字008号