论文部分内容阅读
命题可满足性问题(SAT问题)是第一个被证明的NP完全问题,是一切NP完全问题的“种子”,任何NP完全问题都可在多项式时间内转化为SAT问题进行求解。当前SAT求解方法在测试向量自动生成、符号模型检查及组合等价性检查等电子设计自动化领域中得到了广泛的应用。可见,对SAT问题的研究有着重要的理论意义和应用价值。目前求解SAT问题的主要方法大致可以分为完全算法和不完全算法。如果问题存在解,完全算法保证一定能找到问题的解。但随问题规模增大,SAT问题的计算复杂度呈指数增长;不完全算法虽然不能保证一定能找出问题的解,但是求解速度快且通常能满足需求。故此,不完全算法逐渐成为求解SAT问题的研究热点。本文主要针对不完全算法对SAT问题的求解进行研究。首先介绍了SAT问题及其求解方法、免疫原理与免疫算法的基本知识,其次通过对SAT问题求解和SAT问题全部解问题(ALLSAT问题)求解的研究,提出了两种分别适用于SAT问题和ALLSAT问题求解的改进免疫算法。首先,针对SAT问题的求解,本文提出了一种基于海明距的改进免疫算法。该算法基于海明距对抗体浓度进行定义,避免了耗时的对数计算,提高了算法效率;鉴于传统变异算子存在的不足,算法引入了一种基于随机搜索思想的新变异算子,该变异算子既可以加快种群进化速度,又可以防止进化后期产生“扰动”现象。实验结果表明:该算法在成功率、收敛速度等方面都比基于信息熵的免疫算法有显著提高;与量子克隆免疫算法相比,该算法平均进化代数少、成功率高。其次,针对ALLSAT问题的求解,本文提出了一种改进的多种群克隆免疫算法。该算法采用小生境方法与位爬山算法进行优化,因而具有能保持种群多样性、收敛速度快等优点。算法首先同时进化多个种群,每个种群进行克隆、变异、选择操作,对每个种群的最优个体进行位爬山操作。当子群进化一定代数之后,如该子群的最优解是问题的解,则将该解放入小生境核集。然后比较种群中的个体与小生境集合中个体的距离,如与小生境集合中某个个体距离很小则产生新个体代替该个体构成新子群,然后重新开始多种群进化过程。对ALLSAT问题求解的实验结果表明:对小规模问题该算法能快速的求解出问题的所有解;对于传统方法无法求解的大规模问题,该算法也能尽可能多地找出问题的解。