归结反演的控制策略　

    控制策略的作用就是生成导引图直到产生一棵反演树，其关键在于过程RESOLUTION中的第4步和第5步，即决定选择哪两个子句作归结和实现两个子句的哪个归结。如果对任何一个不可满足的集合S，控制策略都能够从集合S生成一个空子句，则称此控制策略是完备的。我们希望控制策略是完备的、高效的。

    下一页我们将着重介绍以下五种策略：

    1、宽度优先策略

    2、支持集策略

    3、单元优先策略

    4、线性输入形策略

    5、祖先过滤形策略