求解MinSAT问题的加强式格局检测与子句加权算法  

Algorithm of Strengthened Configuration Checking and Clause Weighting for Solving the Minimum Satisfiability Problem

作　　者：周俊萍[1] 任雪亮 殷茜 李睿智[1] 殷明浩[1] ZHOU Jun-Ping　;REN Xue-Liang　;YIN Qian　;LI Rui-Zhi　;YIN Ming-Hao(College of Computer Science and Information Technology,Northeast Normal University,Changchun 130117)

机构地区：[1]东北师范大学计算机科学与信息技术学院,长春130117

出　　处：《计算机学报》2018年第4期745-759,共15页Chinese Journal of Computers

基　　金：国家自然科学基金(61370156;61403076;61403077;61300099);高等学校博士学科点专项科研基金(20120043120017);新世纪优秀人才支持计划(NCET-13-0724);吉林省大型科学仪器装备共享共用专项项目(20150623024TC-03);吉林省青年科研基金项目(20160520104JH)资助

摘　　要：MaxSAT问题的研究已成为一个比较热门的研究领域,与MaxSAT问题相对的是MinSAT问题.MinSAT是SAT问题的另一种优化形式.与MaxSAT问题不同的是MinSAT问题需要找到一组赋值使得可满足的子句数目最少.在求解某些组合优化问题时,将其转化为MinSAT问题比转化为MaxSAT问题有着更快的速度,因此该文提出了一种求解MinSAT问题的加强式格局检测与子句加权局部搜索算法.该算法在随机行走算法的基础上融入了子句加权策略,并根据MinSAT问题本身的特征对格局检测策略进行了加强.加强式格局检测策略通过考查MinSAT问题中变量的环境信息可以减少局部搜索中的循环问题,以此提高局部搜索算法的性能.加强式格局检测策略是格局检测的一种加强.其对格局检测策略的加强主要体现在:当MinSAT问题的环境信息(即格局)发生变化时,仅该变量发生变化的赋值不一定能够作为候选解.只有当格局发生了变化并且格局的变化使得当前考查的子句由不可满足变为可满足时,仅该变量发生变化的赋值(翻转该变量的赋值)才可以作为候选解并向该候选进行解搜索.在局部搜索中,选择合适的变量翻转对提高算法的效率具有重要的意义.如果没有加强式格局检测,对于一般的局部搜索,在变量翻转的时候选择启发值一般是最高的.换言之当格局没有发生变化的时候也允许翻转,这就很可能直接导致上次刚刚翻转的变量又被翻转回来.通过限制只允许格局发生变化且格局的变化使得当前考查的子句由可满足变为不可满足的变量进行翻转,这就会避免上述情况,因此加强格局检测策略在整个搜索过程中都具有重要的意义.子句加权策略通过增加局部最优的代价,使得算法可以进一步找到隐藏在局部最优附近的更好的解,避免了在搜索过程中陷入局部最优.子句加权策略应用在MinSAT问题的基本思想是:对公式F�The maximum satisfiability problem(MaxSAT)has become a popular research field,which has a relative problem-minimum satisfiability problem(MinSAT).MinSAT is another form of satisfiability problem.Unlike MaxSAT problem,MinSAT problems need to find an assignment that can satisfy the least number of clauses.When solving some combinatorial optimization problems,converting them to MinSAT is faster than converting them to MaxSAT.Therefore,we propose a local search algorithm with strengthened configuration checking and clause weighting to solve MinSAT.Based on the random walk local search,the algorithm incorporates the clause weighting strategy and strengthens the configuration checking strategy according to the characteristic of MinSAT.The strengthened configuration checking strategy can reduce the loops by checking the variable environmental information of MinSAT so that the performance of local search algorithm can be improved.The strengthened configuration checking strategy is obtained by strengthening the configuration checking.The strengthening of the configuration checking is mainly embodied in the following aspects.When the environmental information of MinSAT is changed,the assignment with only changing the variable is not able to be as a candidate solution.Only when the environmental information of MinSAT is changed and the changing environmental information could make the current clause satisfied,which is not satisfied before,the assignment with only flipping the variable is able to be as a candidate solution.In the local search algorithm,selecting the appropriate variable to flip plays an important role for improving the efficiency of the algorithm.For the general local search algorithm,if the strengthened configuration checking strategy is not used,the variable with highest heuristic value is usually selected.In other words,the flipping is allowed when the configuration is not changed,which always results in the fact that the last flipping variable is flipped again.The circumstance can be avoided by restricti

关 键 词：最小可满足问题 局部搜索算法 子句加权 格局检测 加强式格局检测 

分 类 号：TP319[自动化与计算机技术—计算机软件与理论]