可满足性求解器算法基于GPU的加速研究

• 作者: 卢凯 王鹤
• 来源期刊: 计算机应用与软件
• 学科: 工学
• 关键词: SAT GPU BCP
• 年，卷（期）: 2011,（10）
• 所属期刊栏目: 基金项目论文
• 页码范围: 58-61
• 分类号: TP311
• 字数: 3950字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-386X.2011.10.017

摘要

可满足性求解(SAT)问题被广泛应用于软件验证、理论证明、微处理器验证、模块验证等领域,工业应用实例问题求解变量规模已达到百万数量级,传统的基于CPU的串行和并行SAT求解方法已无法满足如此规模的问题求解.不同于以往的并行SAT研究,利用GPU并行处理的特点和SAT算法的特点,将SAT算法中最耗时的BCP(Boolean Constraint Propagation)过程并行化,设计实现了基于GPU的BCP过程GP_BCP(GPU Paralleled BCP),从而将BCP过程的性能提高了5.4～10.3倍.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	卢凯	国防科技大学计算机学院	23	241	8.0	15.0
2	王鹤	国防科技大学计算机学院	1	2	1.0	1.0