利用细胞膜演算描述带子句学习的DPLL算法

详细信息    查看全文 | 推荐本文 |

英文篇名：Using membrane calculus to describe DPLL algorithm with clause learning 作者：李壮 ; 刘磊 ; 吕帅 ; 任俊绮 英文作者：LI Zhuang;LIU Lei;LYU Shuai;REN Junqi;College of Computer Science and Technology,Jilin University;Key Laboratory of Symbolic Computation and Knowledge Engineering ( Jilin University) ,Ministry of Education; 关键词：人工智能 ; 问题求解 ; 形式化方法 ; 自动推理 ; DPLL ; 子句学习 ; 演算 ; 细胞膜演算 英文关键词：artificial intelligence;;problem solving;;formal method;;automated reasoning;;DPLL;;clause learning;;calculus;;membrane calculus 中文刊名：HEBG 英文刊名：Journal of Harbin Engineering University 机构：吉林大学计算机科学与技术学院;吉林大学符号计算与知识工程教育部重点实验室; 出版日期：2018-10-30 14:22 出版单位：哈尔滨工程大学学报 年：2019 期：v.40;No.270 基金：国家自然科学基金项目(61300049,61502197,61503044,61763003);; 吉林省科技发展计划项目(20180101053JC) 语种：中文; 页：HEBG201904024 页数：6 CN：04 ISSN：23-1390/U 分类号：163-168

摘要

为了达到推理算法形式化描述的目的,本文采用细胞膜演算的形式化方法描述带子句学习的DPLL算法。分别定义了部分赋值、变元反转、回溯、回跳最大层、细胞膜溶解等反应规则,给出了DPLL的一般过程和冲突分析过程的描述。通过一个算例的求解过程验证了该形式化描述方法的可行性。依赖细胞膜演算可以更直观、简洁地展现推理算法的推理过程,同时展示了膜演算的描述能力和处理能力。
        To formally describe the reasoning algorithm,a formal method of membrane calculus is used to describe DPLL algorithm with clause learning. Some reaction rules are defined,such as partial assignment,variable flip,backtracking,maximum level backjumping,and membrane dissolution. The general process of DPLL and the process of conflict analysis are described. Finally,the feasibility of the formal method is verified by a benchmark solving process. Depending on the membrane calculus,the reasoning process of the DPLL algorithm can be displayed more intuitively and concisely,and the descriptive and processing abilities of the membrane calculus can be shown at the same time.

引文

[1]BEAME P,KAUTZ H,SABHARWAL A.Towards understanding and harnessing the potential of clause learning[J].Journal of artificial intelligence research,2004,22:319-351.
    [2]PIPATSRISAWAT K,DARWICHE A.On the power of clause-learning SAT solvers as resolution engines[J].Artificial intelligence,2011,175(2):512-525.
    [3]AUDEMARD G,LAGNIEZ J M,MAZURE B,et al.On freezing and reactivating learnt clauses[C]//Proceedings of the 14th International Conference on Theory and Applications of Satisfiability Testing.Ann Arbor,MI,USA:Springer,2011:188-200.
    [4]ATSERIAS A,FICHTE J K,THURLEY M.Clause-learning algorithms with many restarts and bounded-width resolution[J].Journal of artificial intelligence research,2011,40:353-373.
    [5]JABBOUR S,LONLAC J,SAIS L,et al.Revisiting the learned clauses database reduction strategies[J].arXiv:1402.1956,2014.
    [6]HEULE M,JRVISALO M,LONSING F,et al.Clause elimination for SAT and QSAT[J].Journal of artificial intelligence research,2015,53:127-168.
    [7]戚正伟,尤晋元.基于细胞膜演算的Web服务事务处理形式化描述与验证[J].计算机学报,2006,29(7):1137-1144QI Zhengwei,YOU Jinyuan.The formal specification and verification of transaction processing in web services by membrane calculus[J].Chinese journal of computers,2006,29(7):1137-1144.
    [8]QI Zhengwei,LI Minglu,FU Cheng,et al.Membrane calculus:a formal method for Grid transactions:research articles[J].Journal concurrency and computation:practice&experience,2006,18(14):1799-1809.
    [9]戚正伟,尤晋元.基于细胞膜演算的Web服务事务处理形式化描述与验证[J].计算机学报,2006,29(7):1137-1144.QI Zhengwei,YOU Jinyuan.The formal specification and verification of transaction processing in web services by membrane calculus[J].Chinese journal of computers,2006,29(7):1137-1144.
    [10]戚正伟.细胞膜演算:一种新的事务处理形式化方法研究[D].上海:上海交通大学,2005.QI Zhengwei.Membrane calculus:a new formal method for transaction processing[D].Shanghai:Shanghai Jiao Tong University,2005.
    [11]任俊绮,刘磊,张鹏.适用于演化过程建模的通信膜演算[J].哈尔滨工程大学学报,2018,39(4):751-759.REN Junqi,LIU Lei,ZHANG Peng.Communication membrane calculus:a formal method for modeling the process of evolution[J].Journal of Harbin Engineering University,2018,39(4):751-759.
    [12]刘磊,刘丰,任俊绮,等.基于细胞膜演算的Dryad形式化描述[J].哈尔滨工程大学学报,2016,37(11):1539-1545.LIU Lei,LIU Feng,REN Junqi,et al.Formal description of Dryad based on membrane calculus[J].Journal of Harbin Engineering University,2016,37(11):1539-1545.
    [13]LUO Mao,LI Chumin,XIAO Fan,et al.An effective learnt clause minimization approach for CDCL SAT solvers[C]//Proceedings of the 26th International Joint Conference on Artificial Intelligence.Melbourne,Australia:IJ-CAI,2017:703-711.
    [14]MOSKEWICZ M W,MADIGAN C F,ZHAO Ying,et al.Chaff:Engineering an efficient SAT solver[C]//Proceedings of the 38th Annual Design Automation Conference.Las Vegas,NV,USA:ACM,2001:530-535.
    [15]AUDEMARD G,SIMON L.Refining restarts strategies for SAT and UNSAT[C]//Proceedings of the 18th International Conference on Principles and Practice of Constraint Programming.Québec City,Canada:Springer,2012:118-126.