《表5 新的子句l值分组情况 (使用CC策略后)》

  提示：宽带有限、当前游客访问压缩模式

本系列图表出处文件名：随高清版一同展现

《一种基于DR算法的构造子句预处理策略》

1. 获取 高清版本忘记账户？点击这里登录

1. 下载图表忘记账户？点击这里登录

接下来完成DR算法的步骤3，又会得到新的子句l值分组情况，如表5所示（加黑体字的是归结而成的子句）。很容易可以得到φ'的定向延伸Ed（φ'）非空，即φ'是可满足的，从而根据定理3得到φ是可满足的。这与用DR算法得出结论相同。