一种结合CCgscore算法的SMT求解技术

来源 :广西民族大学学报：自然科学版 | 被引量 : 0次 | 上传用户：kary_yeah

【摘要】

：

提出了对SMT问题的另一种方法.首先,编译SMT公式并转换为CNF公式.然后充分借鉴求解SAT问题中所用的方法,把它和SMT理论相结合,借鉴在2014SAT竞赛中的CCgscore算法,得到一个满

【作者】

：

连召洋靳庆庚谷涛吴昊

【机构】

：

广西民族大学广西混杂计算与集成电路设计分析重点实验室

【出处】

：

广西民族大学学报：自然科学版

【发表日期】

：

2015年2期

【关键词】

：

可满足性模理论格局配置 CCgscore SMT LAZY CC3

【基金项目】

：

广西研究生教育创新计划项目资助（No.YCSZ2014121）.

下载到本地 , 更方便阅读

下载此文赞助VIP

声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架

论文部分内容阅读

提出了对SMT问题的另一种方法.首先,编译SMT公式并转换为CNF公式.然后充分借鉴求解SAT问题中所用的方法,把它和SMT理论相结合,借鉴在2014SAT竞赛中的CCgscore算法,得到一个满足CNF公式的解.最后把得到的当前解与T-solver进行交互并且检查其在特定理论背景下的可满足性.由于在SMT求解的过程中结合了先进的CCgscore算法,所以在求解某些SMT问题时效果比较好.

其他文献

军事屯田背景下北宋西北地区生态环境变迁

入宋以来，由于宋夏战事的需要，北宋在西北黄土高原一带开展了大规模屯田活动。随着战事的发展，屯田的规模、范围也在不断扩大，但是西北地区无论从地貌还是从气候上看，都不适合农业

期刊

屯田西北地区生态环境变迁Army Reclamation Northwest Region Ecological Changes

试论宋代农业信仰

在宋代,农业信仰与农业生产有着密切联系,贯穿在整个农业生产之中,在乡村社会里非常盛行。宋代农业信仰在调节民众心理、丰富民众文化生活、稳定社会秩序、加强社会凝聚力等

期刊

宋代农业信仰乡村社会Song Dynasty Agriculture Belief Rural Society

现代企业形象设计的启示与研究

分析徽商老字号的品牌特色与品牌文化内涵,探讨其在相当长的一段历史时期内可持续发展的成功策略,为现代企业品牌形象设计与推广寻找文化基因.

期刊