基于CDCL与遗传算法的SAT求解器算法的研究

作     者：臧婉君 

作者单位：西安电子科技大学 

学位级别：硕士

导师姓名：李培咸

授予年度：2018年

学科分类：12[管理学] 1201[管理学-管理科学与工程(可授管理学、工学学位)] 081104[工学-模式识别与智能系统] 08[工学] 0835[工学-软件工程] 0811[工学-控制科学与工程] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

主      题：可满足性问题 遗传算法 CDCL算法 SAT混合求解器 

摘      要：可满足性问题（SAT问题）是计算机科学领域中的核心基础问题,是寻找并确定一组真值指派作为以合取范式形式（CNF）表示的给定布尔约束公式的解决方案的问题。解决方案是一组布尔真值指派,可以对原公式进行真值评估。SAT问题具有广泛的应用领域,包括计算机辅助设计,人工智能,路线规划等。可以将各种电子设计自动化（EDA）应用程序（如等效性检查,模型检查,测试模式生成,布局和路线）定义或转化为SAT问题。至今为止国内外许多研究都致力于开发高度可扩展和高效的SAT求解器。SAT问题是NP完全问题,如果该问题的解是存在的,SAT求解器会尝试为原公式找到解决方案。尽管在许多实际情况下可以通过最先进的SAT求解器在合理的计算资源消耗内去求解很多问题,但由于SAT的NP完全性,在很多情况下求解工作仍然非常困难。本论文提出了一种基于增强型遗传算法（GA）和冲突驱动子句学习算法（CDCL）的SAT完备混合求解器。这个求解器是一个完备求解器,可以在SAT问题的求解工作上得到一个完整的解决方案,或者证明解决方案不存在（即原问题是不可满足（UNSAT）问题）,它可以在所有三类SAT实例测试集（应用类,随机类和特制类）上都表现得相对好。这种求解器的主要混合方法是使用结合局部搜索技术的遗传算法作为求解器不完备部分的算法,并且集成了 CDCL算法的求解器作为互补的完备部分。其结合了预处理,布尔约束传播,冲突分析,子句学习,边界点等求解技术,并考虑了 GA求解阶段中问题规模（变量数与子句数的比例）与遗传参数的具体设置方式。这种混合机制是让两个部分相互指导共同求解,从而找到原问题的解决方案,并且能够避免单纯依赖某一部分求解器来独自寻找解决方案的过程的出现。通过与原基于CDCL算法或GA算法的SAT求解器的一系列实验数据进行比较,本文实现的混合求解器是完备求解器,可以高效地解决不同类别的SAT问题,比现存的常用求解器具有更快的求解速度并在运行过程中消耗合理的较多内存,且测试集的问题规模由小到大是十分广泛的。特别是针对基于CDCL算法的求解器Minisat不容易求解或限定时间内无法判定求解结果的某些测试集上,本文提出的求解器求解效率更高,求解时间大幅度减少。与Minisat求解器相比,本文提出的混合求解器在最佳实例上的平均求解时间为0.56倍。当在GA部分中依照问题规模的不同而设置适当的遗传算子组合机制和参数时,实验结果显示出此求解器能够同时减少求解时间并降低内存消耗量。在本研究中问题规模最大的测试例上,此求解器平均求解时间为前者的0.76倍,且平均内存用量减少了 38%。经过大量针对不可满足的UNSAT测试集的对比实验结果得出,此求解器不仅能够在限定求解时间内Minisat无法证明不可满足性的测试集上成功求解,更能够比Minisat在更短的求解时间内得出解决方案,体现出了不可满足性证明方面更为优秀的求解能力,并且展示了应用了 GA而不是单一地应用SLS作为混合求解器不完备算法部分的优势。本文所提出的完备求解器充分地结合了 GA和CDCL两者的优势,展示出在更多的SAT问题上可表现出更佳性能的潜力,更体现了在后续科研方向上优化意义和在实际应用问题上的应用前景。