论文部分内容阅读
最大可满足性(MaximumSatisfiability,MaxSAT)问题、最大团(MaximumClique,MC)问题、最大公共子图(MaximumCommoninducedSubgraph,MCS)问题是计算机科学中经典的NP难问题,也是人工智能、运筹学等领域的经典组合优化问题。三个问题是解决实际问题的有效模型,其高效的完备算法的设计具有重要的理论意义和实践意义。
MaxSAT、MC和MCS的优化目标不同,但是都可归约为如何解决冲突问题。冲突是指不存在合理的方案满足给定的约束条件。MaxSAT的冲突是指在任何真值指派下均存在不满足子句;MC的冲突是不相邻的顶点不能同时构建团;MCS的冲突是顶点匹配不满足边约束条件,构成公共子图的顶点匹配数降低。MaxSAT子句冲突检测的技术可以发现MC、MCS问题中顶点之间隐藏的冲突关系。找到的冲突越多,分支限界算法的界的质量越高,搜索分支越少。
基于找到更多冲突、有效改进界的思路,深入研究了以上三个代表性的NP难问题,设计了基于分支限界的高效完备算法。
(1)对MaxSAT问题,提出了三个优化冲突集的策略,有效地改进了MaxSAT算法的下界。推理规则优先是优先使用子句消耗最小的推理规则,再使用单子句传播、失败文字检测等检测冲突的方法。单子句排序是优先传播其相反文字在二元子句中出现次数最多的单子句,达到优先发现小规模冲突集的目的。进一步失败文字检测是扩大失败文字搜索的范围,沿搜索树向前看两步,找到了大规模冲突集。上述三个优化策略多途径地获得更多冲突集,提高了下界。糅合了优化策略的Maxsatz2013算法在2013年MaxSAT评估赛中取得优秀的成绩,在随机类别组排名第一,在构造类别组排名第二。
(2)对MaxSAT问题,提出了环式展开规则,解决了长度大于3的环式结构不能使用推理规则的问题。环式展开规则通过找到含有与第一蕴含点相同文字的单子句,去除环式结构,并使得新增子句从2(n-2)个三元子句变换为n个简单的二元子句。实验结果显示相比同期最好的分支限界完备算法ahmaxsat-ls-1.55,糅合了环式展开规则的Brmaxsat多解决了20个Max2SAT算例,并缩短了平均求解时间。
(3)对MC问题,提出了权重覆盖的概念并设计了基于权重覆盖的顶点划分函数,以最小化分支数。传统的上界计算方法偏重顶点的邻接关系,独立集的权重通常是固定的,这使得最大加权团的上界比较松弛。基于权重覆盖的独立集划分通过动态改变独立集的权重,解决了独立集覆盖顶点权重的多种冲突,有效地减少了搜索树分支。权重覆盖的划分方式具有较小的时间复杂度,而实验结果表明基于权重覆盖的WC-MWC算法在大规模稀疏图上,相比同期最好的WLMC,WC-MWC算法将相关算例的求解速度提高了4倍。在78%的算例上,WC-MWC求解效率超过了最好的启发式算法FastWCLq。
(4)对MCS问题,原创性地提出了结合强化学习的分支策略以更快地找到算法的最优解。未匹配顶点提供的最大可匹配数越少,上界的质量越好。通过学习历史搜索过程,以上界下降幅度量化分支顶点造成的冲突,并设计了价值函数,以计算分支顶点得到的累计奖励。结合强化学习的新分支策略按照分值的降序选择顶点;当出现平局时,再选择度最大的顶点。新策略改进了传统分支策略仅依赖图的静态属性即顶点度的不足,使得分支顶点的选择更多样化,算法可以快速地到达叶节点。基于强化学习的分支策略算法McSplit+RL,在2万多个大规模子图同构算例上,比目前最好的最大公共子图算法McSplit多解出了130个算例。
以上研究表明,对于具体的NP难问题,找到其本质的冲突形式从而找到解决冲突的办法,能有效提高完备算法的求解效率。
MaxSAT、MC和MCS的优化目标不同,但是都可归约为如何解决冲突问题。冲突是指不存在合理的方案满足给定的约束条件。MaxSAT的冲突是指在任何真值指派下均存在不满足子句;MC的冲突是不相邻的顶点不能同时构建团;MCS的冲突是顶点匹配不满足边约束条件,构成公共子图的顶点匹配数降低。MaxSAT子句冲突检测的技术可以发现MC、MCS问题中顶点之间隐藏的冲突关系。找到的冲突越多,分支限界算法的界的质量越高,搜索分支越少。
基于找到更多冲突、有效改进界的思路,深入研究了以上三个代表性的NP难问题,设计了基于分支限界的高效完备算法。
(1)对MaxSAT问题,提出了三个优化冲突集的策略,有效地改进了MaxSAT算法的下界。推理规则优先是优先使用子句消耗最小的推理规则,再使用单子句传播、失败文字检测等检测冲突的方法。单子句排序是优先传播其相反文字在二元子句中出现次数最多的单子句,达到优先发现小规模冲突集的目的。进一步失败文字检测是扩大失败文字搜索的范围,沿搜索树向前看两步,找到了大规模冲突集。上述三个优化策略多途径地获得更多冲突集,提高了下界。糅合了优化策略的Maxsatz2013算法在2013年MaxSAT评估赛中取得优秀的成绩,在随机类别组排名第一,在构造类别组排名第二。
(2)对MaxSAT问题,提出了环式展开规则,解决了长度大于3的环式结构不能使用推理规则的问题。环式展开规则通过找到含有与第一蕴含点相同文字的单子句,去除环式结构,并使得新增子句从2(n-2)个三元子句变换为n个简单的二元子句。实验结果显示相比同期最好的分支限界完备算法ahmaxsat-ls-1.55,糅合了环式展开规则的Brmaxsat多解决了20个Max2SAT算例,并缩短了平均求解时间。
(3)对MC问题,提出了权重覆盖的概念并设计了基于权重覆盖的顶点划分函数,以最小化分支数。传统的上界计算方法偏重顶点的邻接关系,独立集的权重通常是固定的,这使得最大加权团的上界比较松弛。基于权重覆盖的独立集划分通过动态改变独立集的权重,解决了独立集覆盖顶点权重的多种冲突,有效地减少了搜索树分支。权重覆盖的划分方式具有较小的时间复杂度,而实验结果表明基于权重覆盖的WC-MWC算法在大规模稀疏图上,相比同期最好的WLMC,WC-MWC算法将相关算例的求解速度提高了4倍。在78%的算例上,WC-MWC求解效率超过了最好的启发式算法FastWCLq。
(4)对MCS问题,原创性地提出了结合强化学习的分支策略以更快地找到算法的最优解。未匹配顶点提供的最大可匹配数越少,上界的质量越好。通过学习历史搜索过程,以上界下降幅度量化分支顶点造成的冲突,并设计了价值函数,以计算分支顶点得到的累计奖励。结合强化学习的新分支策略按照分值的降序选择顶点;当出现平局时,再选择度最大的顶点。新策略改进了传统分支策略仅依赖图的静态属性即顶点度的不足,使得分支顶点的选择更多样化,算法可以快速地到达叶节点。基于强化学习的分支策略算法McSplit+RL,在2万多个大规模子图同构算例上,比目前最好的最大公共子图算法McSplit多解出了130个算例。
以上研究表明,对于具体的NP难问题,找到其本质的冲突形式从而找到解决冲突的办法,能有效提高完备算法的求解效率。