| 一种结合CCgscore算法的SMT求解技术 |
| |
| 引用本文： | 连召洋,靳庆庚,谷涛,吴昊.一种结合CCgscore算法的SMT求解技术[J].广西民族大学学报,2015,21(2). |
| |
| 作者姓名： | 连召洋 靳庆庚 谷涛 吴昊 |
| |
| 作者单位： | 广西民族大学广西混杂计算与集成电路设计分析重点实验室,南宁,530006 |
| |
| 基金项目： | 广西研究生教育创新计划项目资助 |
| |
| 摘 要： | 提出了对SMT问题的另一种方法.首先,编译SMT公式并转换为CNF公式.然后充分借鉴求解SAT问题中所用的方法,把它和SMT理论相结合,借鉴在2014SAT竞赛中的CCgscore算法,得到一个满足CNF公式的解.最后把得到的当前解与T-solver进行交互并且检查其在特定理论背景下的可满足性.由于在SMT求解的过程中结合了先进的CCgscore算法,所以在求解某些SMT问题时效果比较好.
|
| 关 键 词： | CCgscore 可满足性模理论 Lazy 格局配置 |
A New SMT Solver Combined with CCgscore Algorithm |
| |
| LIAN Zhao-yan,JIN Qing-geng,GU Tao,WU Hao.A New SMT Solver Combined with CCgscore Algorithm[J].Journal of Guangxi University For Nationalities(Natural Science Edition),2015,21(2). |
| |
| Authors: | LIAN Zhao-yan JIN Qing-geng GU Tao WU Hao |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
