论文部分内容阅读
CDCL(Conflict Driven Clause Learning)SAT求解器在形式验证等领域应用广泛,在实际应用中的大量NP问题已经被证明可以转化为SAT问题进行求解,因此,SAT问题的求解效率备受关注。目前已经有很多在工业界广泛应用的求解器,但求解器中的重启策略众多且参数控制复杂,导致通常选择默认参数设置进行求解,从而降低求解器的效率和易用性。为了提高CDCL SAT求解器的实用性,本文以典型的CDCL算法为基础,对SAT求解器重启策略进行研究。本课题来源于国家自然科学基金资助项目,本文的研究内容如下:(1)本文首先对SAT问题的发展进行调研,深入分析了DP算法(Davis Putnam Algorithm)、DPLL算法(Davis Putnam Logemann Loveland)、GRASP算法(Genetic Search Algorithm for the SAT Problem)、SATO算法(Satisfiability Testing Optimized)、Chaff算法、BerkMin算法(Berkeley-Minsk Algorithm)、Glucose算法等代表性的CDCL SAT算法的特点,以及典型求解器的突破性技术;(2)进行详细的实验设计,分析重启序列、重启间隔、间隔增长系数等因素对实例求解效率的影响,从个体差异性、群体差异性、重启序列影响三个方面进行分析;(3)在分析重启策略对求解效率影响的基础上,进一步用7种重启策略集合覆盖97%案列的最优重启策略;提取求解初期(未进行重启)的特征数据,分析求解初期的特征值变化与相应的所重启策略之间的关系。实验结果表明,通过改变重启策略可以提高求解效率。在所选的测试集上,通过改变重启策略所得的最优解比缺省解的效率平均相差411%;重启策略在求解过程中表现出较大的个体差异性和一定的群体差异性;相比重启频率,重启序列对求解效率影响更大。综合分析发现,可满足性问题比不可满足问题存在更大的改进空间。通过求解初期的特征值变化频率与相应的重启策略进行关联,将SAT问题的特征和后面最优重启策略建立关联关系,为后期分析SAT问题特征而选择最优重启策略提供技术支持。