Page 129 - 《软件学报》2021年第9期

李壮 等:基于局部搜索的并行扩展规则推理方法 2753

4 总结与展望

本文基于 ERACC 算法提出了并行框架,提出了 PERACC 算法,我们先后提出了预处理、化简解空间等技
术,并行处理各个子空间.通过实验显示:该算法较原算法的求解效率有较大的提高,并不断缩短了与国际著名
算法 SWCC 的差距.
PERACC 算法在原有算法的基础上进一步大胆地尝试了扩展规则方法领域中不完备推理的发展.下一步,
我们决定将 DPLL 算法中的单文子传播机制加入其中,从而进一步完善预处理的效果.另一方面,我们将知识约
简方法应用于并行前和并行后,通过对复杂问题约简手段的不断提高,才能让我们去不断地求解复杂性更高、
规模更大的测试用例.具体的方法还需要进一步进行理论分析和大量的实验来证明想法的可行性,合理与
PERACC 结合,使算法的求解能力得到最大化的提升.

References:
[1] Selman B, Levesque HJ, Mitchell DG. A new method for solving hard satisfiability problems. In: Proc. of the 10th National Conf.
on Artificial Intelligence. 1992. 400−446.
[2] Li CM, Huang WQ. Diversification and determinism in local search for satisfiability. In: Proc. of the 8th Int’l Conf. on Theory and
Applications of Satisfiability Testing. 2005. 158−172.
[3] Li CM, Li Y. Satisfying versus falsifying in local search for satisfiability. In: Proc. of the 15th Int’l Conf. on Theory and
Applications of Satisfiability Testing. 2012. 477−478.
[4] KhudaBukhsh AR, Xu L, Hoos HH, Leyton-Brown K. SATenstein: Automatically building local search SAT solvers from
components. Artificial Intelligence, 2016,232(4):20−42.
[5] Cai SW, Su KL. Local search with configuration checking for SAT. In: Proc. of the 23rd IEEE Int’l Conf. on Tools with Artificial
Intelligence. 2011. 59−66.
[6] Cai SW, Su KL. Local search for Boolean satisfiability with configuration checking and subscore. Artificial Intelligence, 2013,
204(9):75−98.
[7] Luo C, Cai SW, Su KL, Wu W. Clause states based configuration checking in local search for satisfiability. IEEE Trans. on
Cybernetics, 2015,45(5):1014−1027.
[8] Luo C, Cai SW, Wu W, Jie Z, Su KL. CCLS: An efficient local search algorithm for weighted maximum satisfiability. IEEE Trans.
on Computers, 2015,64(7):1830−1843.
[9] Cai SW, Jie Z, Su KL. An effective variable selection heuristic in SLS for weighted Max-2-SAT. Journal of Heuristics, 2015,21(3):
433−456.
[10] Cai SW, Zhang XD. ReasonLS. In: Proc. of the SAT COMPETITION 2018 Solver and Benchmark Descriptions. 2018. 52−53.
[11] Lin H, Sun JG, Zhang YM. Theorem proving based on the extension rule. Journal of Automated Reasoning, 2003,31(1):11−21.
[12] Wu X, Sun JG, Lü S, Li Y, Meng W, Yin MH. Improved propositional extension rule. In: Proc. of the 1st Int’l Conf. on Rough Sets
and Knowledge Technology. 2006. 592−597.
[13] Sun JG, Li Y, Zhu XJ, Lü S. A novel theorem proving algorithm based on extension rule. Journal of Computer Research and
Development, 2009,46(1):9−14 (in Chinese with English abstract).
[14] Zhang LM, Ouyang DT, Bai HT. Theorem proving algorithm based on semi-extension rule. Journal of Computer Research and
Development, 2010,47(9):1522−1529 (in Chinese with English abstract).
[15] Yin MH, Sun JG, Lin H, Wu X. Possibilistic extension rules for reasoning and knowledge compilation. Ruan Jian Xue Bao/Journal
of Software, 2010,20(11):2826−2837 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/3690.htm [doi: 10.3724/
SP.J.1001.2010.03690]
[16] Liu L, Niu DD, Lü S. Knowledge compilation methods based on the hyper extension rule. Chinese Journal of Computers, 2016,
39(8):1681−1696 (in Chinese with English abstract).
[17] Wang Q, Liu L, Lü S. #SAT solving algorithms based on extension rule using heuristic strategies. Ruan Jian Xue Bao/Journal of
Software, 2018,29(11):3517−3527 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5298.htm [doi: 10.13328/j.
cnki.jos.005298]