《表1 CNF公式φ：一种基于DR算法的构造子句预处理策略》

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

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

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

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

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

如表1所示为一个CNF公式φ，Ci（1≤i≤21）是φ中的子句。为了更好的比较出CC策略的效果，首先使用DR算法求解出φ的可满足性。如表2所示φ中子句按最大的变元角标值l分配到相应bucket组中的情况。计算出每个子句最大的变元角标值l。即:l（C1）=4，l（C2）=5，l（C3）=19，l（C4）=9，l（C5）=21，l（C6）=12，l（C7）=21，l（C8）=12，l（C9）=10，l（C10）=9，l（C11）=15，l（C12）=15，l（C13）=16，l（C14）=17，l（C15）=11，l（C16）=19，l（C17）=8，l（C18）=13，l（C19）=20，l（C20）=6，l（C21）=17。