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

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