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

A Novel Local Search-Based Extension Rule Reasoning Method

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

Extension rule was proposed by Lin et al.in 2003,which is a new rule in automated reasoning.As a“complementary”reasoning method with resolution by Martin Davis,an expert in artificial intelligence,extension rule-based reasoning methods have been widely recognized around the world.Lots of excellent achievements which related to extension rule were proposed in succession,such as knowledge compilation,possibilistic possibility reasoning and model counting methods.Especially in knowledge compilation,a theory called EPCCL(each pair contains complementary literal),which was the result of extension rule-based knowledge compilation method,was highly appreciated by Murray and Rosenthal.Throughout the achievements related to extension rule,the main researches on extension rule are among the aspects of complete reasoning methods,and researches among incomplete reasoning methods were rare.The original algorithm of extension rule is high memory consumption owing to the process of inclusion-exclusion principle,which results in being replaced by NER(novel extension rule).Transforming mode of the maximum term is the key of NER,and transforming in order guarantees the completeness of NER.Owing to the unintelligent transforming mode of the maximum term in NER,the scale of formulae it can handle are still very small.In this paper,after analyzing the relevance of extension rule and local search,the concept of“maximum term”in logic is utilized,which aimed at designing and implementing the novel reasoning framework of extension rule based on local search.In order to accelerate the computing in greedy mode,a method for computing scores based on different sets is proposed.On this basis,to make the searching process of maximum terms more suitable for the framework,two implementations of accurately configuration checking for different scale of formulae are proposed,which are based on the proposal of algorithm SWCC(smoothed weighting with configuration checking).After that,for further limitation of selecting variables,a new strategy called double-sided semi-extension rule is proposed,whose inspiration comes from SER(semi-extension rule)in 2009.Based on the framework and heuristics mentioned above,the first incomplete reasoning algorithm in extension rule called ERACC(extension rule based on accurate configuration checking)is designed and implemented.The experimental results show that the algorithm ERACC greatly breakthrough the bottleneck of performance in the reasoning methods related to extension rule,and get much improved in the ability of processing formulae with large scale.In the problems of random instances and structured instances,algorithm ERACC outperforms several existed reasoning methods based on extension rule.In addition,the robustness of ERACC has shown among the benchmarks used above.The comparison with state-of-the-art solvers in performance shows that ERACC is still not better than state-of-the-art solvers,but it also has comparative performance with some of them,which shows the great potential of algorithm ERACC.The proposal of ERACC is the first step of the researches of incomplete reasoning framework,and it shows the meaning for exploring more powerful heuristics to make the framework much stronger.This framework makes the extension rule no longer restricted by the scale of formulae,and it can also be used in the field of knowledge compilation and possibilistic possibility reasoning.