[1]李壮,刘磊,吕帅,等.利用细胞膜演算描述带子句学习的DPLL算法[J].哈尔滨工程大学学报,2019,40(04):799-804.[doi:10.11990/jheu.201709122]
 LI Zhuang,LIU Lei,LYU Shuai,et al.Using membrane calculus to describe DPLL algorithm with clause learning[J].hebgcdxxb,2019,40(04):799-804.[doi:10.11990/jheu.201709122]
点击复制

利用细胞膜演算描述带子句学习的DPLL算法(/HTML)
分享到:

《哈尔滨工程大学学报》[ISSN:1006-6977/CN:61-1281/TN]

卷:
40
期数:
2019年04期
页码:
799-804
栏目:
出版日期:
2019-04-05

文章信息/Info

Title:
Using membrane calculus to describe DPLL algorithm with clause learning
作者:
李壮1 刘磊1 吕帅12 任俊绮1
1. 吉林大学 计算机科学与技术学院, 吉林 长春 130012;
2. 吉林大学 符号计算与知识工程教育部重点实验室, 吉林 长春 130012
Author(s):
LI Zhuang1 LIU Lei1 LYU Shuai12 REN Junqi1
1. College of Computer Science and Technology, Jilin University, Changchun 130012, China;
2. Key Laboratory of Symbolic Computation and Knowledge Engineering(Jilin University), Ministry of Education, Changchun 130012, China
关键词:
人工智能问题求解形式化方法自动推理DPLL子句学习演算细胞膜演算
分类号:
TP181
DOI:
10.11990/jheu.201709122
文献标志码:
A
摘要:
为了达到推理算法形式化描述的目的,本文采用细胞膜演算的形式化方法描述带子句学习的DPLL算法。分别定义了部分赋值、变元反转、回溯、回跳最大层、细胞膜溶解等反应规则,给出了DPLL的一般过程和冲突分析过程的描述。通过一个算例的求解过程验证了该形式化描述方法的可行性。依赖细胞膜演算可以更直观、简洁地展现推理算法的推理过程,同时展示了膜演算的描述能力和处理能力。

参考文献/References:

[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, JÄRVISALO 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:IJCAI, 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.

相似文献/References:

[1]孙宇嘉,王晓鸣,贾方秀,等.封锁雷智能防排系统[J].哈尔滨工程大学学报,2014,(05):580.[doi:10.3969/j.issn.10067043.201303071]
 SUN Yujia,WANG Xiaoming,JIA Fangxiu,et al.An intelligent anti removal system for blockage mines[J].hebgcdxxb,2014,(04):580.[doi:10.3969/j.issn.10067043.201303071]
[2]李颖,杨罡,李占山.维持弧的唯一性优化粗粒度弧相容算法[J].哈尔滨工程大学学报,2018,39(04):744.[doi:10.11990/jheu.201610104]
 LI Ying,YANG Gang,LI Zhanshan.Optimized coarse-grained arc-consistency algorithm for maintaining the uniqueness of arc[J].hebgcdxxb,2018,39(04):744.[doi:10.11990/jheu.201610104]

备注/Memo

备注/Memo:
收稿日期:2017-09-28。
基金项目:国家自然科学基金项目(61300049,61502197,61503044,61763003);吉林省科技发展计划项目(20180101053JC).
作者简介:李壮,男,博士研究生;刘磊,男,教授,博士生导师;吕帅,男,副教授,硕士生导师.
通讯作者:吕帅,E-mail:lus@jlu.edu.cn
更新日期/Last Update: 2019-04-03