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

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

基于格局检测的模型计数方法

模型计数是指求出给定命题公式的模型数,是SAT问题的泛化.模型计数在人工智能领域取得了广泛应用,很多现实问题都可以规约为模型计数进行求解.目前,常用的模型计数求解器主要有Cachet与sharp SAT,它们均采用完备方法且具有高效的求解能力,但其求解效率对模型数不敏感.有理由猜测:当给定问题的模型较少时,不完备算法可能发挥其效率优势而更适合模型计数.局部搜索是求解SAT问题的高效不完备方法,Cai等人提出了格局检测策略,并将其应用到局部搜索方法中,提出了SWcc算法,具有很高的求解效率.对SWcc算法进行扩充,分别得到了迭代法与优化后的增量法两种效率较高的不完备模型计数方法,给出了两种方法的思路和具体实现.最后给出了大量测试样例的实验结果,以验证当给定合取范式的模型较少时,该迭代法与优化后的增量法的求解效率有所提升.

基于格局检测的并行模型计数方法

在经典的可满足性问题求解中,针对处理模型数较少的实例,SWcc迭代法和SWcc优化增量法与完备的模型计数方法相比,求解适用性更高,但SWcc迭代法和SWcc优化增量法均为串行求解方法,没有对解空间进行剪枝、化简等处理。本文基于此设计了基于格局检测的并行模型计数算法。该算法以化简解空间和启发式为核心,将原解空间分解成为若干子空间并对原子句集进行化简后,并行处理各个子空间。实验结果表明:对于模型个数较少、公式规模较大的问题,该算法比原算法更具有适用性。

结合格局检测与局部搜索的故障数据缩减方法

针对集成电路故障诊断中故障数据缩减方法 N-cover存在冗余故障数据的问题,提出了结合格局检测与局部搜索的故障数据缩减方法。通过分析故障数据与端口覆盖次数的逻辑关系,提出了故障频率和故障覆盖度的概念以指导局部搜索。同时,结合格局检测策略以避免重复搜索,进而通过减少冗余迭代来增加搜索广度。在标准测试用例上的实验结果表明,与现有方法相比,本文方法可有效缩减故障数据数目并提高求解效率。

基于个体稳定度博弈的动态社区发现算法研究

在动态网络中发现社区结构是一个复杂而又有重要意义的课题。该文针对动态网络中的社区发现问题,提出一种基于个体稳定度的博弈论方法(PDG)。在该博弈方法中,网络中的每个节点都是一个独立个体。个体会根据网络中的其他个体的状态,使用最佳应对策略进行社区的选择。针对网络演化过程中的社区更新问题,该文提出了格局检测(Configuration checking)等优化策略,从而大大提高了演化网络的社区发现的效率。最后,在真实演化网络的实验中,与最新的静态和动态社区发现方法进行对比,验证了PDG方法的效率和效果。

基于IAPS的扩展规则局部搜索算法

ERACC(Extension Rule Based on Accurate Configuration Checking)算法由杨洋等人基于扩展规则和格局检测提出,具有较高的推理效率.为进一步提高ERACC算法在大规模SAT(Satisfiability)问题求解上的性能,本文在搜索由极大项组成的空间时,首先利用IMOM(Improved Maximum Occurrences on Clauses of Maximum Size)思想生成初始极大项,接着设计了适用于扩展规则推理的CCA_ER(Configuration Checking with Aspiration for Extension Rule-Based Reasoning)启发式策略,为极大项中格局信息未发生变化的变量对应文字提供一定的翻转机会.同时,为进一步提高扩展规则推理算法在k-SAT问题求解上的性能,设计了适用于扩展规则推理的PAWS_ER(Pure Additive Weighting Scheme for Extension Rule-Based Reasoning)策略,并且给出变量的Subscore_ER(Subscore for Extension Rule-Based Reasoning),CScore_ER(Comprehensive Score for Extension Rule-Based Reasoning)和HScore_ER(Hybrid Score for Extension Rule-Based Reasoning)属性.在此基础上,提出了ERACC_IAPS(ERACC with IMOM,CCA_ER,PAWS_ER and Subscore_ER)和CERACC_IAPS(ERACC with IMOM,CCA_ER,PAWS_ER,CScore_ER and HScore_ER)算法.实验结果表明:ERACC_IAPS和CERACC_IAPS算法的效率明显优于ERACC算法,最高可将其求解效率提高1000多倍.

基于局部搜索的并行扩展规则推理方法

扩展规则推理方法在经典的可满足性问题求解中已得到广泛应用,若干个基于扩展规则的推理方法已被提出,皆得到国内外的认可,例如完备的NER,IMOMH_IER,PPSER算法以及基于局部搜索的不完备算法ERACC等,都具有良好的求解效果.其中,ERACC算法是当前扩展规则求解器中求解效率最高、能力最强的算法.但是,串行的ERACC算法在启发式和预处理上仍然具有可提升的空间.基于此,设计了相应的并行框架,提出了PERACC算法.该算法基于格局检测的局部搜索方法,从变量赋初始值、化简解空间和启发式这3个阶段出发,将原极大项空间分解成为若干极大项子空间,并对原子句集进行化简后,并行处理各个子空间.通过实验显示:该算法与原算法相比,不仅在求解效率方面有较大提高,而且可以求解规模更大的测试用例,使扩展规则方法再次突破公式规模的限制.

一种新的基于局部搜索的扩展规则推理方法

作为与归结推理方法互补的推理方法,扩展规则推理方法得到了国内外广泛认可.目前扩展规则推理方法的研究主要集中于完备推理方法,由于极大项变换方式过于机械,导致该方法处理公式的规模比较局限.该文在深入分析扩展规则推理和局部搜索关联性的基础上,利用子句集中的"极大项"概念设计了一种反向求解策略,进而设计并实现一种新的基于局部搜索的扩展规则推理框架.在此基础上,为了使得极大项搜索过程更加适配该框架,提出了一种基于精确格局检测实现和双向半扩展规则策略的两阶段局部搜索算法.实验结果表明,该文提出的基于精确格局检测的新型扩展规则推理算法ERACC突破了传统扩展规则推理对公式规模的局限,求解效率有了极大提高,使得扩展规则推理方法不再受公式规模制约,可以用于知识编译和可能性推理等多方面的应用.