归结反演搜索策略及应用技术

归结反演过程可以很容易地被描述为“运用归结规则直到产生空子句为止”，但是对子句集进行归结时，一个关键问题是决定选取哪两个子句作归结。如果对任意一对可以归结的子句都作归结，这样不仅消耗很多的时间，而且会产生许多无用的归结式， 占用了很多空间，降低了效率。为此，需要研究有效的归结控制或搜索策略。

（一）排序策略

按什么序列执行归结，这个问题与在状态空间中下一步将要扩展哪个节点的问题类似。

例如，可以使用宽度优先或者深度优先策略。

在这里，把原始子句（包括待证明合式公式的否定的子句形）叫作0层归结式。（i+1）层的归结式是一个i层归结式和一个j（j≤i）层归结式进行归结所得到的归结式。

宽度优先就是先生成第1层所有的归结式，然后是第2层所有的归结式，依次类推，直到产生空子句结束，或不能再进行归结为止。深度优先是产生一个第1层的归结式，然后用第l层的归结式和第0层的归结式进行归结，得到第2层的归结式，依次类推，直到产生空子句结束，或者不能归结，则回溯到其他的上层子句继续归结。

排序策略的另一个策略是单元优先（Unit Preference）策略，即在归结过程中优先考虑仅由一个文字构成的子句，这样的子句称为单元子句。

（二）精确策略

精确策略不涉及被归结子句的排序，它们只允许某些归结发生。这里主要介绍三种精确归结策略。

1.支持集（SetofSupport）策略

支持集策略就是指，每次归结时，参与归结的子句中至少应有一个是由目标公式的否定所得到的子句，或者是它们的后裔。(www.xing528.com)

所谓后裔是指，如果（I）α2是α1与另外某子句的归结式，或者（II）α2是α1的后裔与其他子句的归结式，则称α2是α1的后裔，α1是α2的祖先。

支持集策略是完备的，即假如对一个不可满足的子句集合运用支持集策略进行归结，那么最终会导出空子句。

如果将子句P∨Q作为目标公式的否定所得到的子句，则该图所示的归结过程满足支持集策略。

2.线性输入（Linear Input）策略

线性输入策略是指，参与归结的两个子句中至少有一个是原始子句集中的子句（包括那些待证明的合式公式的否定）。

线性输入策略是不完备的。例如，对于子句集合。该集合是不可满足的，但是无法用线性输入归结得到结果。

3.祖先过滤（Ancestry Filtering）策略

由于线性输入策略不完备，改进该策略则得到祖先过滤策略：参与归结的两个子句中至少有一个是初始子句集中的句子，或者是另一个子句的祖先。该策略是完备的。对于上面的子句集合，可以有如图5-1所示的归结反演树。

图5-1　归结反演树