首页 > 期刊 > 自然科学与工程技术 > 信息科技 > 电子信息科学综合 > 计算机工程与科学 > 基于一阶逻辑的可满足求解方法研究进展 【正文】
摘要:基于命题逻辑的布尔可满足SAT存在描述能力弱、抽象层次低、求解复杂度高等问题,而基于一阶逻辑的可满足性模理论SMT采用高层建模语言,表达能力更强,更接近于字级设计,避免将问题转化到位级求解,在硬件RTL级验证、程序验证与实时系统验证等领域得到了广泛应用。针对近年来涌现的众多SMT求解方法,依据方法的求解方式进行了分类与对比。而后,对3种主流的求解方法Eager方法、Lazy方法和DPLL(T)方法的实现进行了概要介绍。最后,讨论了SMT求解方法当前所面临的主要挑战以及在SMT求解方面的一些研究成果,并对今后的研究进行了展望。
注:因版权方要求,不能公开全文,如需全文,请咨询杂志社
一对一咨询服务、简单快捷、省时省力
了解更多 >直邮到家、实时跟踪、更安全更省心
了解更多 >去除中间环节享受低价,物流进度实时通知
了解更多 >正版杂志,匹配度高、性价比高、成功率高
了解更多 >