会议专题

PSA_SAT:求解SAT问题的退火算法并行研究

可满足性(SAT)问题是命题逻辑中一个经典问题,也是计算机科学理论与应用的一个核心问题,广泛应用于软件验证,数字系统测试与验证等领域.工业应用实例问题求解变量规模己达到百万数量级,传统的基于CPU的串行和并行SAT求解方法已无法满足如此规模的问题求解.本文基于GPU设计并实现了一种新的并行SAT求解器-PSA_SAT.不同于现有的并行SAT算法,PSA_SAT将SAT问题转化成数学极值问题,通过模拟退火算法来实现求解,运用启发式策略对一般的退火算法进行改进以加速收敛,并利用CUDA编程模型实现并行.实验表明,对于随机生成的测试用例,改进后的模拟退火算法优于一般的退火算法,且经过GPU加速后PSA_SAT相对于MiniSat获得了更好的求解性能.

可满足性求解 模拟退火 启发式策略

王鹤 卢凯

国防科技大学计算机学院,湖南长沙 410073

国内会议

2010年全国软件与应用学术会议(NASAC2010)

苏州

中文

29-36

2010-11-04(万方平台首次上网日期,不代表论文的发表时间)