作者:
李壮
关键词:
DPLL；子句学习；细胞膜演算
摘要:
尽管命题逻辑中可满足性问题是NP-完全问题，但仍然存在SAT求解器能在当今计算机领域很多的相关现实问题。对于结构化问题，最快的SAT求解器是基于回溯程序的被称之为DPLL算法，扩展额外的技术如子句学习。伴随子句学习的DPLL是快速完备Boolean可满足性求解器的重要过程。DPLL方法是最经典的求解SAT问题的完备方法，基于对二叉树进行深度优先搜索的思想，通过对原子进行真值指派快速降低子句集规模。直到近些年，用DPLL解决SAT问题已经有效的应用于现实当中。其主要原因是算法的改进，其中基于DPLL的SAT求解器关键技术是子句学习。子句学习是一种扩展的DPLL方法，可以简单的理解为在真值指派发生冲突时，分析冲突产生的原因，找到产生冲突的子句并记录，以便实现非时序回溯，并防止在接下来的搜索过程发生相同的冲突。 通常情况下，一个事务和一个或多个子事务的嵌套可以用细胞膜结构的嵌套来表达。而事务的一般活动可用反应规则来描述，这一点和一般的Petri网类似。一种新的事务处理形式化方法——细胞膜演算，从语法、操作语义、表达能力以及重写逻辑语义等方面描述移动事务和动态变化的事务处理过程。细胞膜的语法和操作语义采用了生物学中的细胞膜模型，细胞膜不但可以嵌套，链接上下文的概念，其本身还可以移入移出、溶解和生成。在操作语义上采用的化学抽象模型，因此细胞膜演算具有与图灵机等价的表达能力。细胞膜演算是细胞膜计算的一个扩充，细胞膜计算强调的是过程，细胞膜演算主要突出的是表达能力。相比较于细胞膜计算，膜演算增加了一些反应规则，是一种新的事务处理形式化方法。 子句学习采用了搜索剪枝技术、蕴含图等强大的冲突分析过程，更加快了学习的效率。但是目前为止，形式化的子句学习描述仍然不够完善。例如，在指派某一层的过程中，不能直观的表现当前层的状态；当前层发生第一次冲突后，使变量反转强制取反，这时的状态该如何体现（冲突或者满足）。诸如此类问题，用细胞膜演算描述，可更加直观，更加层次分明的体现出整个DPLL的过程。 本文所采用抽象的表推演，用细胞膜演算，形式化的描述了带有子句学习的DPLL算法。对DPLL的一般过程、子句学习过程进行抽象描述，为子句学习过程提供了形式化验证。本文将基于细胞膜演算从两个方面描述：细胞膜描述DPLL的一般过程，以及对冲突的分析（子句学习）的过程。并以一个实际例子加以验证。从而达到证明细胞膜演算可以形式化描述DPLL、子句学习全过程的目的。更直观、简洁的表达了整个学习的过程，为DPLL算法提供了一种崭新的形式化描述方法，同时也推动了膜演算在计算机领域的发展。
在线下载