《表4 φ'的子句l值分组情况》

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

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

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

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

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

由于φ有21个子句，要删除7个子句，根据CC策略和序列d0，构造子句为:（），从而要删除的子句就是含有x6和x11的子句，即C3，C6，C10，C13，C15，C19，C20。从φ删除这些子句后得到一个新的CNF公式φ'。使用DR算法确定φ'是否是可满足的。如表4所示φ'中子句按最大的变元角标值l分配到相应bucket组中的情况。