赋权MAX-SAT问题的动态凸化方法

论文摘要

可满足性问题（简称SAT问题）在运筹学、人工智能、VLSI集成电路设计与检测和计算机科学等热点领域有着广泛的应用，SAT问题是第一个被证明为NP-hard的问题。解决SAT问题具有突出的理论和应用价值。完备算法求解SAT问题要花费大量时间且只能解决小规模的SAT问题，所以很难应用到实际的问题。上世纪九十年代以来，有关SAT问题的算法研究转向不完备的搜索算法的研究，不完备算法虽然不能保证一定能找到解，但可以有效地解决大规模的SAT问题。赋权MAX-SAT问题是SAT问题的推广，求解赋权MAX-SAT问题的算法同样适用于SAT问题。本文对GRASP和GRASP+PR算法进行了研究，总结了提高算法性能和跳出局部陷阱所用的策略或机制。用局部搜索算法求解SAT问题遇到的主要瓶颈在于如何避免陷入局部最优解或如何跳出陷入的局部最优解，以提高计算效率。本文的主要研究目的就是通过有效途径来合理地解决如何使算法在陷入局部最优值的情况下跳出来。文献[50,51]提出了一种解决非线性约束的非线性整数规划问题的局部搜索方法。该方法采用辅助函数变换使原问题转化成一新的组合优化问题，并证明在解的可行域里新问题的最优解是原问题的最优解；结合局部搜索策略，在极小化辅助函数的过程中，当算法陷入局部极小解时，通过增加一个参数的值能使辅助函数成功且有效的跳出之前收敛的局部最优解。上述描述的方法称为动态凸化方法[50,51],我们将其推广到解决SAT问题，通过与GRASP和GRASP+PR算法在多个标准实例的计算试验对比，表明基于动态凸化方法的算法有较快的收敛速度。其次，我们将动态凸化方法应用到解决图着色问题（简称GCP问题）中。通过构造辅助函数及利用FM局部搜索算法，我们用构造的算法对不同规模的图着色问题实例进行实验，并与已知的GRASP算法对比；计算结果表明，用局部搜索算法求解变换后的组合优化问题的解的质量高于用局部搜索算法直接求解原GCP问题。最后，对局部搜索算法进行实验分析；对本文的求解SAT及GCP问题的局部搜索算法研究进行总结并做相应的工作展望。

论文目录

• 中文摘要
• Abstract
• 目录
• 第一章 引言
• 1.1 论文的研究背景
• 1.2 SAT 问题的定义
• 1.3 SAT 问题在集成电路设计中的应用
• 1.4 论文的研究任务
• 第二章 GRASP 及 GRASP+PR 算法的研究
• 2.1 GRASP 及 GRASP+PR 算法介绍
• 2.2 GRASP 算法
• 2.3 GRASP+PR 算法
• 2.4 GRASP 和 GRASP+PR 对比
• 第三章 赋权 MAX-SAT 问题的动态凸化方法
• 3.1 引言
• 3.2 距离、邻域及局部搜索算法
• 3.3 MAX-WSAT 辅助函数及其性质
• 3.4 辅助函数的局部搜索算法
• 3.5 实验分析
• 3.6 结论
• 第四章 图着色问题的动态凸化方法研究
• 4.1 引言
• 4.2 概念定义
• 4.3 辅助函数定义
• 4.4 GCP 的动态凸化方法
• 4.5 局部搜索算法的实验分析
• 4.6 结论
• 第五章 总结
• 5.1 本文的主要工作
• 5.2 展望
• 参考文献
• 致谢
• 个人简历、在学期间的研究成果及发表的学术论文