﻿ 利用细胞膜演算描述带子句学习的DPLL算法
«上一篇
 文章快速检索 高级检索

 哈尔滨工程大学学报  2019, Vol. 40 Issue (4): 799-804  DOI: 10.11990/jheu.201709122 0

### 引用本文

LI Zhuang, LIU Lei, LYU Shuai, et al. Using membrane calculus to describe DPLL algorithm with clause learning[J]. Journal of Harbin Engineering University, 2019, 40(4), 799-804. DOI: 10.11990/jheu.201709122.

### 文章历史

1. 吉林大学 计算机科学与技术学院, 吉林 长春 130012;
2. 吉林大学 符号计算与知识工程教育部重点实验室, 吉林 长春 130012

Using membrane calculus to describe DPLL algorithm with clause learning
LI Zhuang 1, LIU Lei 1, LYU Shuai 1,2, REN Junqi 1
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
Abstract: 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.
Keywords: artificial intelligence    problem solving    formal method    automated reasoning    DPLL    clause learning    calculus    membrane calculus

Davis和Putnam等提出DPLL算法是求解SAT问题的完备算法。先进的SAT求解器普遍基于回溯的DPLL算法，其中包含了子句学习(clause learning)等技术[1-3]

P系统是一种细胞膜计算模型[7-8]。该模型相继出现了许多变型，其中多半表达能力都与图灵机等价。根据细胞新陈代谢的特点如：消融、分裂或创建等，可知膜系统的格局及它们之间转移的概念[9-10]

1 伴随子句学习的DPLL算法 1.1 DPLL过程与子句学习

1) P←Unit propagate

2) If P assigns a value to every variable

3)    return success

4) Else

5)    P contains a conflict

6)   choose a conflict graph G to find c under P and add it to F

7)   rollback variable or back jump

1.2 冲突分析

1.3 重启机制

2 细胞膜演算 2.1 基本概念

1) Σ是一个有限非空的类型集合，包含所有出现对象的类型；

2) μ是一个细胞膜结构，包含m个细胞膜；

3) Oi(1≤im)是第i个细胞膜的对象多集；

4) Ri(1≤im)是第i个细胞膜的反应规则多集；

5) C是类型映射函数，定义为oOiΣ。该函数定义对象o的类型C(o)→Σ。直观上讲，所有对象都是类型化的。

2.2 语法

 $M,M':: = 0\left| {\left[ {{}_iO,R,M} \right]} \right|M,M'$
 $O,O':: = 0\left| {a:T} \right|OO'$
 $\begin{array}{l} R,R':: = 0\left| {O \to O'} \right|O \to {{O'}_{{\rm{out}}}}\left| {O \to {{O'}_{{\rm{in}}\left( f \right)}}} \right|\\ \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;O \to \lambda \left| R \right|R' \end{array}$
 $\lambda :: = \delta \left| {\delta k} \right|\eta k\left| M \right.$

2.3 反应规则

 $\left[ {{}_iOO'',O \to O'\left| {R',M} \right.} \right] \to \left[ {{}_iO'O'',O \to O'\left| {R',M} \right.} \right]$

 $\begin{array}{l} \left[ {{}_iO',R,\left[ {{}_jO'O'',O \to {{O''}_{{\rm{out}}}}\left| {R',M} \right.} \right]M} \right] \to \left[ {{}_iO'O''',} \right.\\ \left. {R,\left[ {{}_jO''O \to {{O''}_{{\rm{out}}}}\left| {R',M'} \right.} \right]M} \right] \end{array}$

 $\begin{array}{l} \left[ {{}_iOO',O \to {{O''}_{{\rm{in}}\left( j \right)}}\left| R \right.,\left[ {{}_jO''',R',M'} \right]M} \right] \to \left[ {{}_iO',} \right.\\ \left. {O \to {{O''}_{{\rm{in}}\left( j \right)}}\left| R \right.,\left[ {{}_jO''O''',R',M'} \right]M} \right] \end{array}$

 $\left[ {{}_iO'',R,\left[ {{}_jOO',O \to \delta \left| {R',M'} \right.} \right]M} \right] \to \left[ {{}_iO'',O',R,M} \right]$

 $\begin{array}{l} \left[ {{}_iO'',R,\left[ {{}_jOO',O \to \sigma i\left| {R',M'} \right.} \right]M} \right] \to \left[ {{}_iO'',R,} \right.\\ \left. M \right]\left[ {{}_jOO',O \to \sigma i\left| {R',M'} \right.} \right] \end{array}$

 $\begin{array}{l} \left[ {{}_iO'',R,M} \right]\left[ {{}_jOO',O \to \eta i\left| {R',M'} \right.} \right] \to \left[ {{}_iO'',R,} \right.\\ \left. {\left[ {{}_jOO',O \to \eta i\left| {R',M'} \right.} \right]M} \right] \end{array}$

 $\left[ {{}_iOO',O \to M\left| {R',M'} \right.} \right] \to \left[ {{}_iO',O \to M\left| {R,MM'} \right.} \right]$

3 细胞膜演算描述子句学习 3.1 细胞膜演算规则

1) 部分赋值(细胞膜的产生)。

 $\left[ {{}_i{l_i}L,{l_i} \to M'\left| {R',M} \right.} \right] \to \left[ {_iL,{l_i} \to M'\left| {R',MM'} \right.} \right]$

2) 变元反转。

 $\left[ {{}_i{l_i}L,{l_i} \to \neg {l_i}\left| {R,M} \right.} \right] \to \left[ {{}_i\neg {l_i}L,{l_i} \to \neg {l_i}\left| {R,M} \right.} \right]$

3) 回溯。

 $\left[ {{}_i{l_i}L,{l_i} \to \neg {l_{i - 1}}\left| {R,M} \right.} \right] \to \left[ {{}_i\neg {l_{t - 1}}L,{l_i} \to \neg {l_{i - 1}}\left| {R,M} \right.} \right]$

4) 回跳最大层。

 $\left[ {{}_i{l_i}L,{l_i} \to \neg {l_t}\left| {R,M} \right.} \right] \to \left[ {{}_i\neg {l_t}L,{l_i} \to \neg {l_t}\left| {R,M} \right.} \right]$

5) 细胞膜溶解。

 $\left[ {_iL,R,\left[ {{}_jl,l \to \delta \left| {R',M'} \right.} \right]M} \right] \to \left[ {_iL,R,M} \right]$
3.2 细胞膜演算描述DPLL

 $O = \left( {{p_i},\neg {q_i},\neg {q_{i - 1}},q,r,v,\neg v,\emptyset ,S,{T_p},{F_p},{T_q},{F_q},y} \right)$
 ${M_0} = \left[ {S,{R_1},{M_j}} \right]$
 ${R_0} = \left( {{r_{01}},{r_{02}},{r_{03}},{r_{04}},{r_{05}}} \right)$
 ${r_{01}}:{p_i} \to {T_p}\left| {{F_p}} \right.;{T_p} \to {T_p}{M_{11}}\left| {{F_p} \to {F_p}{M_{10}}} \right.$
 ${r_{02}}:q \to {T_q}\left| {{F_q}} \right.$
 ${r_{03}}:{T_p} \to {T_{{\rm{pin}}M11}};{F_q} \to {F_{{\rm{pin}}M10}}$
 ${r_{04}}:\left( {v,\neg v} \right) \to {\left( {v,\neg v} \right)_{{\rm{in}}\left( j \right)}},y \to \delta$
 ${r_{05}}:S \to {\emptyset _{{\rm{out}}}}$
 ${\rho _0} = \left\{ {{r_{04}} > {r_{02}} > {r_{01}} > {r_{03}} > {r_{05}}} \right\}$
 ${R_j} = \left\{ {{r_{j1}},{r_{j2}}} \right\}$
 ${r_{j1}}:{p_i} \to \neg {p_{{\rm{iout}}}}$
 ${r_{j2}}:{p_i} \to \neg {p_{i - 1{\rm{out}}}}$
 ${\rho _j} = {r_{j1}} > {r_{j2}}$
 Download: 图 1 DPLL过程对应的细胞膜嵌套关系 Fig. 1 Nested relationship of membranes corresponding to DPLL process

DPLL求解首先对决策变元进行赋值。r01:piTp|Fp; TpTpM11|FpFpM10对决策变元p进行赋值，若决策变元p赋值为T，则会产生新的子细胞膜M11。同理，若决策变元p赋值为F，会产生另一个新的子细胞膜M10

r04:(v, $\neg$v)→(v, $\neg$v)in(j), yδ中，y为冲突层细胞膜。当出现冲突(v, $\neg$v)时，子句集剩余部分移入判定膜(v, $\neg$v)in(j)，细胞膜yδ溶解。

3.3 冲突分析

 $\begin{array}{*{20}{c}} {{M_C} = \left[ {{\rm{Begin}}:{\rm{State}},{R_1},{M_0},{M_L},{M_J}} \right]}\\ {{M_0} = \left[ {_00,{R_0},0} \right]}\\ {{M_L} = \left[ {_L0,{R_L},0} \right]}\\ {{M_F} = \left[ {_F0,{R_F},0} \right]}\\ {{M_J} = \left[ {_J0,{R_J},0} \right]} \end{array}$
 $\begin{array}{*{20}{c}} {{R_1} = }\\ {{\rm{Begin}}:{\rm{State}} \to {\rm{Begi}}{{\rm{n}}_0}:{\rm{State}}{_{\left( {{\rm{in}}\left( 0 \right)} \right.}}|}\\ {{\rm{Succes}}{{\rm{s}}_0}:{\rm{State}} \to {\rm{Begi}}{{\rm{n}}_1}:{\rm{State}}{_{{\rm{in}}\left( L \right)}}|}\\ {{\rm{Succes}}{{\rm{s}}_{\rm{L}}}:{\rm{State}} \to {\rm{Begi}}{{\rm{n}}_{\rm{F}}}:{\rm{State}}{_{{\rm{in}}\left( F \right)}}|}\\ {{\rm{Fai}}{{\rm{l}}_0}:{\rm{State}} \to {\rm{Learnin}}{{\rm{g}}_0}:{\rm{State}}{_{{\rm{in}}\left( L \right)}}}\\ {{\rm{Fai}}{{\rm{l}}_1}:{\rm{State}} \to {\rm{Judge}}:{\rm{State}}{_{\left( {{\rm{in}}} \right)J}}|}\\ {{\rm{Fai}}{{\rm{l}}_{0'}}:{\rm{State}} \to {\rm{Learnin}}{{\rm{g}}_{0'}}:{\rm{State}}{_{{\rm{in}}\left( F \right)}}|}\\ {{\rm{Fai}}{{\rm{l}}_{\rm{L}}}:{\rm{State}} \to {\rm{Learnin}}{{\rm{g}}_0}:{\rm{State}}{_{{\rm{in}}\left( F \right)}}} \end{array}$
 $\begin{array}{*{20}{c}} {{R_0} = }\\ {{\rm{Begi}}{{\rm{n}}_0}:{\rm{State}} \to {{\rm{L}}_0}:{\rm{State}}|}\\ {{{\rm{L}}_0}:{\rm{State}} \to {\rm{Succes}}{{\rm{s}}_0}:{\rm{State}}{_{{\rm{out}}}}|}\\ {{{\rm{L}}_0}:{\rm{State}} \to {\rm{Fail:}}{\rm{State}}{_{{\rm{out}}}}} \end{array}$
 $\begin{array}{*{20}{c}} {{R_L} = }\\ {{\rm{Begin}}{{\rm{L}}_1}:{\rm{State}} \to {{\rm{L}}_1}:{\rm{State}}|}\\ {{{\rm{L}}_1}:{\rm{State}} \to {\rm{SuccessL:}}{\rm{State}}{_{{\rm{out}}}}|}\\ {{{\rm{L}}_1}:{\rm{State}} \to {\rm{Fai}}{{\rm{l}}_0}{\rm{:}}{\rm{State}}{_{{\rm{out}}}}|}\\ {{\rm{Fai}}{{\rm{l}}_0}{\rm{:}}{\rm{State}} \to {\rm{Learnin}}{{\rm{g}}_0}:{\rm{State}}{_{{\rm{out}}}}|}\\ {{\rm{Learnin}}{{\rm{g}}_0}:{\rm{State}} \to {\rm{Fai}}{{\rm{l}}_0}{\rm{:}}{\rm{State}}{_{{\rm{out}}}}} \end{array}$
 $\begin{array}{*{20}{c}} {{R_F} = }\\ {{\rm{Begin}}{{\rm{L}}_1}:{\rm{State}} \to {{\rm{L}}_F}:{\rm{State}}}\\ {{{\rm{L}}_F}:{\rm{State}} \to {\rm{Success:}}{\rm{State}}{_{{\rm{out}}}}}\\ {{{\rm{L}}_1}:{\rm{State}} \to {\rm{Fai}}{{\rm{l}}_1}{\rm{:}}{\rm{State}}{_{{\rm{out}}}}|}\\ {{\rm{Learnin}}{{\rm{g}}_{0'}}:{\rm{State}} \to {\rm{Fail:}}{\rm{State}}{_{{\rm{out}}}}|}\\ {{\rm{Learnin}}{{\rm{g}}_L}:{\rm{State}} \to {\rm{Fai}}{{\rm{l}}_{\rm{L}}}{\rm{:}}{\rm{State}}{_{{\rm{out}}}}} \end{array}$
 $\begin{array}{*{20}{c}} {{R_J} = }\\ {{\rm{Begi}}{{\rm{n}}_J}:{\rm{State}} \to {\rm{Fai}}{{\rm{l}}_L}:{\rm{State|}}}\\ {{\rm{Fai}}{{\rm{l}}_{\rm{I}}}:{\rm{State}} \to {\rm{Fai}}{{\rm{l}}_{0'}}:{\rm{Stat}}{{\rm{e}}_{{\rm{out}}}}|}\\ {{\rm{Fai}}{{\rm{l}}_{\rm{I}}}:{\rm{State}} \to {\rm{Fai}}{{\rm{l}}_L}:{\rm{Stat}}{{\rm{e}}_{{\rm{out}}}}} \end{array}$

4 算例验证

 $例\;\;\;\;\;\;\left[ {\begin{array}{*{20}{c}} {p \vee q \vee r}\\ {s \vee \neg r \vee p}\\ {\neg s \vee \neg t}\\ {u \vee \neg q}\\ t \end{array}} \right]$

 $\begin{array}{l} \left[ {{}_0t\left| {{S_0},t \to T,{S_0} \to {S_1},M} \right.} \right] \to \left[ {{}_1T\left| {{S_1},t \to T,} \right.} \right.\\ \left. {{S_0} \to {S_1},M} \right] \end{array}$
 $\begin{array}{l} \left[ {{}_1s\left| {{S_1},s \to F,{S_0} \to {S_1},M} \right.} \right] \to \left[ {{}_1F\left| {{{S'}_1},S \to F,} \right.} \right.\\ \left. {{S_1} \to {{S'}_1},M} \right] \end{array}$
 $\begin{array}{l} \left[ {{}_1u\left| {{{S'}_1},S \to F,{S_1} \to {{S'}_1},M} \right.} \right] \to \left[ {{}_2F\left| {{S_2},u \to F,} \right.} \right.\\ \left. {{{S'}_1} \to {S_2},M} \right] \end{array}$
 $\begin{array}{l} \left[ {{}_2q\left| {{S_2},q \to F,{S_2} \to {{S'}_2},M} \right.} \right] \to \left[ {{}_2F\left| {{{S'}_2},q \to F,} \right.} \right.\\ \left. {{S_2} \to {{S'}_2},M} \right] \end{array}$
 $\begin{array}{l} \left[ {{}_2p\left| {{{S'}_2},p \to F,{{S'}_2} \to {S_3},M} \right.} \right] \to \left[ {{}_3F\left| {{S_3},p \to F,} \right.} \right.\\ \left. {{{S'}_2} \to {S_3},M} \right] \end{array}$
 $\begin{array}{l} \left[ {{}_3r\left| {{S_3},r \to T,{S_3} \to {{S'}_3},M} \right.} \right] \to \left[ {{}_3T\left| {{{S'}_3},r \to T,} \right.} \right.\\ \left. {{S_3} \to {{S'}_3},M} \right] \end{array}$
 $\begin{array}{l} \left[ {{}_3\left( {r,\neg r} \right)\left| {{{S'}_3}} \right.,\left( {r,\neg r} \right) \to \emptyset ,{s_3} \to \emptyset ,M} \right] \to \\ \left[ {{}_3\emptyset \left| \emptyset \right.,{{S'}_3}\left( {r,\neg r} \right) \to \emptyset ,{S_3} \to \emptyset ,M} \right] \end{array}$
 $\begin{array}{l} \left[ {{}_2p\left| {{{S'}_2},p \to T,{{S'}_2} \to {S_3},M} \right.} \right] \to \left[ {{}_2T\left| {{{S'}_3},p \to F,} \right.} \right.\\ \left. {{{S'}_2} \to {S_3},M} \right] \end{array}$

5 结论

1) 采用细胞膜演算的形式化方法描述带子句学习的DPLL算法，分别定义了部分赋值、变元反转、回溯、回跳最大层、细胞膜溶解等反应规则，给出了DPLL的一般过程和冲突分析过程的描述。最后通过一个算例来验证该形式化方法是可行的。

2) 选用计算机领域中最成功的SAT求解方法进行刻画，使得整个推理过程可以与细胞膜演算过程完全对应，展现了细胞膜演算的描述能力。

 [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. DOI:10.1613/jair.1410 (0) [2] PIPATSRISAWAT K, DARWICHE A. On the power of clause-learning SAT solvers as resolution engines[J]. Artificial intelligence, 2011, 175(2): 512-525. DOI:10.1016/j.artint.2010.10.002 (0) [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. (0) [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. DOI:10.1613/jair.3152 (0) [5] JABBOUR S, LONLAC J, SAIS L, et al. Revisiting the learned clauses database reduction strategies[J]. arXiv: 1402.1956, 2014. (0) [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. DOI:10.1613/jair.4694 (0) [7] 戚正伟, 尤晋元. 基于细胞膜演算的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. DOI:10.3321/j.issn:0254-4164.2006.07.015 (0) [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. (0) [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. DOI:10.3321/j.issn:0254-4164.2006.07.015 (0) [10] 戚正伟.细胞膜演算: 一种新的事务处理形式化方法研究[D].上海: 上海交通大学, 2005. QI Zhengwei. Membrane calculus: a new formal method for transaction processing[D]. Shanghai: Shanghai Jiao Tong University, 2005. (0) [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. (0) [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. (0) [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. (0) [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. (0) [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. (0)