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

       摘要: MaxSAT问题的研究已成为一个比较热门的研究领域,与MaxSAT问题相对的是MinSAT问题.MinSAT是SAT问题的另一种优化形式.与MaxSAT问题不同的是MinSAT问题需要找到一组赋值使得可满足的子句数目最少.在求解某些组合优化问题时,将其转化为MinSAT问题比转化为MaxSAT问题有着更快的速度,因此该文提出了一种求解MinSAT问题的加强式格局检测与子句加权局部搜索算法.该算法在随机行走算法的基础上融入了子句加权策略,并根据MinSAT问题本身的特征对格局检测策略进行了加强.加强式格局检测策略通过考查MinSAT问题中变量的环境信息可以减少局部搜索中的循环问题,以此提高局部搜索算法的性能.加强式格局检测策略是格局检测的一种加强.其对格局检测策略的加强主要体现在:当MinSAT问题的环境信息(即格局)发生变化时,仅该变量发生变化的赋值不一定能够作为候选解.只有当格局发生了变化并且格局的变化使得当前考查的子句由不可满足变为可满足时,仅该变量发生变化的赋值(翻转该变量的赋值)才可以作为候选解并向该候选进行解搜索.在局部搜索中,选择合适的变量翻转对提高算法的效率具有重要的意义.如果没有加强式格局检测,对于一般的局部搜索,在变量翻转的时候选择启发值一般是最高的.换言之当格局没有发生变化的时候也允许翻转,这就很可能直接导致上次刚刚翻转的变量又被翻转回来.通过限制只允许格局发生变化且格局的变化使得当前考查的子句由可满足变为不可满足的变量进行翻转,这就会避免上述情况,因此加强格局检测策略在整个搜索过程中都具有重要的意义.子句加权策略通过增加局部最优的代价,使得算法可以进一步找到隐藏在局部最优附近的更好的解,避免了在搜索过程中陷入局部最优.子句加权策略应用在MinSAT问题的基本思想是:对公式F中的每个子句都赋予一个权值1,MinSAT问题求解算法在搜索过程中一旦陷入局部最优就增加在当前解下可满足子句的权值,这使得算法能跳出局部最优并向更好方向搜索.实验结果表明,该算法可以有效求解MinSAT问题,并且在大规模实例中具有良好的表现,这也在一定程度上说明了加强式格局检测策略和子句加权策略的有效性.

作者:
周俊萍 任雪亮 殷茜 李睿智 殷明浩
单位:
东北师范大学计算机科学与信息技术学院 长春130117
出处:
《 计算机学报》
刊期:
2018年第0卷第4期
基金:
国家自然科学基金(61370156,61403076,61403077,61300099) 高等学校博士学科点专项科研基金(20120043120017) 新世纪优秀人才支持计划(NCET-13-0724) 吉林省大型科学仪器装备共享共用专项项目(20150623024TC-03) 吉林省青年科研基金项目(20160520104JH)

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

摘要:MaxSAT问题的研究已成为一个比较热门的研究领域,与MaxSAT问题相对的是MinSAT问题.MinSAT是SAT问题的另一种优化形式.与MaxSAT问题不同的是MinSAT问题需要找到一组赋值使得可满足的子句数目最少.在求解某些组合优化问题时,将其转化为MinSAT问题比转化为MaxSAT问题有着更快的速度,因此该文提出了一种求解MinSAT问题的加强式格局检测与子句加权局部搜索算法.该算法在随机行走算法的基础上融入了子句加权策略,并根据MinSAT问题本身的特征对格局检测策略进行了加强.加强式格局检测策略通过考查MinSAT问题中变量的环境信息可以减少局部搜索中的循环问题,以此提高局部搜索算法的性能.加强式格局检测策略是格局检测的一种加强.其对格局检测策略的加强主要体现在:当MinSAT问题的环境信息(即格局)发生变化时,仅该变量发生变化的赋值不一定能够作为候选解.只有当格局发生了变化并且格局的变化使得当前考查的子句由不可满足变为可满足时,仅该变量发生变化的赋值(翻转该变量的赋值)才可以作为候选解并向该候选进行解搜索.在局部搜索中,选择合适的变量翻转对提高算法的效率具有重要的意义.如果没有加强式格局检测,对于一般的局部搜索,在变量翻转的时候选择启发值一般是最高的.换言之当格局没有发生变化的时候也允许翻转,这就很可能直接导致上次刚刚翻转的变量又被翻转回来.通过限制只允许格局发生变化且格局的变化使得当前考查的子句由可满足变为不可满足的变量进行翻转,这就会避免上述情况,因此加强格局检测策略在整个搜索过程中都具有重要的意义.子句加权策略通过增加局部最优的代价,使得算法可以进一步找到隐藏在局部最优附近的更好的解,避免了在搜索过程中陷入局部最优.子句加权策略应用在MinSAT问题的基本思想是:对公式F中的每个子句都赋予一个权值1,MinSAT问题求解算法在搜索过程中一旦陷入局部最优就增加在当前解下可满足子句的权值,这使得算法能跳出局部最优并向更好方向搜索.实验结果表明,该算法可以有效求解MinSAT问题,并且在大规模实例中具有良好的表现,这也在一定程度上说明了加强式格局检测策略和子句加权策略的有效性.

说明:如本页面涉及到版权问题或作者不愿意公开,请联系本站管理员删除!

0.289830s