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

作     者：王鹤 卢凯 Wang He;Lu Kai

作者机构：国防科技大学计算机学院湖南长沙410073 

基　　金：国家重点基础研究发展计划项目(2005CB321801) 霍英东基金(111072) 

出 版 物：《计算机应用与软件》 (Computer Applications and Software)

年 卷 期：2011年第28卷第10期

页      码：58-61页

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

主 题 词：SAT GPU BCP 

学科分类：08[工学] 0835[0835] 081202[081202] 0812[工学-测绘类] 

D　O　I：10.3969/j.issn.1000-386X.2011.10.017

馆 藏 号：203441947...