论文部分内容阅读
Max-SAT问题是一个著名的约束满足问题，在理论研究和实际应用中都有重要的意义。局部搜索框架是一个非常有效的解决带权重的Max-SAT问题的框架，本文提出了一种新的启发式的变量选择方法——CCTriplex，它对于基于局部搜索框架的Max-SAT算法提升很大，特别是带权重的Max-2-SAT实例。 这种新的启发式的变量选择方法是根据最近提出的格局检测策略设计出来的。格局检测策略已经被成功运用于多个SAT求解算法中，包括2012年的SAT比赛冠军CCASat。CCTriplex策略将变量分成三大类来进行挑选，最优先挑选的变量是那些Score大于等于0并且满足格局检测要求的那些变量;接着是不满足格局检测要求但是Score大于0的变量;最后挑选的是那些Score小于0满足格局检测要求的变量。根据CCTriplex策略本文开发出一个新的基于启发式局部搜索框架的用于解带权重的Max-SAT问题的算法——CCMaxSAT。 我们在结构化和随机的Max-2-SAT实例上以及随机的Max-3-SAT实例上都测试了CCMaxSAT的效果，并将在Max-2-SAT实例上的CCMaxSAT解得的效果同另一个很高效的在Max-2-SAT上的算法ITS，2012年Max-SAT比赛中评价最高的局部搜索求解器ubcsat-IRoTS和一个非常著名的完备解法器wMaxSATz解出的效果做了对比。在所有的随机实例上，CCMaxSAT求得的解的质量显著的超出了ITS、ubcsat-IRoTS的解的质量;在一类著名的结构化实例Frb实例上， CCMaxSAT和ITS分别在不同的实例上有优势，但是总体上看CCMaxSAT略微好于ITS。在稀疏的Max-2-SAT的实例中（比2还要小的比率）CCMaxSAT同wMaxSATz也非常有竞争力，50％以上的实例都解出了最优解。在稠密的Max-2-SAT实例和Frb实例中，CCMaxSAT解出的解都要好于wMaxSAT解出的解。另外，在随机的Max-3-SAT实例上，CCMaxSAT也远远优于ubcsat-IRoTS。 为了更好的比较CCTriplex策略与格局检测策略的效率，在CCMaxSAT代码基础上开发了一个基于格局检测的局部搜索算法CCMaxSAT_org，它们的区别只在于用的是格局俭测策略还是CCTriplex策略。通过选择每个实例组中典型的实例让两个算法运行比较，发现CCTriplex策略在Max-2-SAT和Max-3-SAT问题上确实更加高效。另外，本文通过详细的实验分析，理解了算法不同搜索步的执行频率，以及它们和实例密度的关系。这些分析可以指导我们根据不同的密度设计不同的启发式策略。