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

• 作者: 吴昊 谷涛 连召洋 靳庆庚
• 来源期刊: 广西民族大学学报（自然科学版）
• 学科: 工学
• 关键词: CCgscore 可满足性模理论 Lazy 格局配置
• 年，卷（期）: 2015,（2）
• 所属期刊栏目: 计算机技术
• 页码范围: 66-68
• 页数: 3页
• 分类号: TP301.6
• 字数: 1987字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	靳庆庚	广西民族大学广西混杂计算与集成电路设计分析重点实验室	6	3	1.0	1.0
2	吴昊	广西民族大学广西混杂计算与集成电路设计分析重点实验室	6	2	1.0	1.0
3	谷涛	广西民族大学广西混杂计算与集成电路设计分析重点实验室	3	3	1.0	1.0
4	连召洋	广西民族大学广西混杂计算与集成电路设计分析重点实验室	2	0	0.0	0.0