《表5 Blocksworld类问题实例的实验结果》

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

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

《基于格局检测的模型计数方法》

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

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

（s）

上述结构化实例中，合取范式中包含的子句不全是3-SAT，有些子句仅包含两个或多个文字.而SWcc算法的优势在于求解3-SAT子句，故求解结构化实例的效率比求解随机化实例效率有所下降.在求解模型数为1的子句时，不完备方法仍具有优势.值得注意的是，表4中的AIM类实例的模型数均为1是测试样例的特点，而不是人为选取.对于该类实例，Cachet求解时间是优化后的增量法与迭代法求解时间的2倍以上.sharpSAT求解时间是优化后的增量法与迭代法求解时间的1.5倍以上.对于表5中的模型数为1的blocksworld类实例，Cachet求解时间为本文所提两种算法求解时间的3倍～4倍.sharpSAT求解时间为本文提出的两种算法求解时间的2倍～3倍.对于模型数为2的实例medium，本文提出的两种算法同样具有优势.对于PARITY类实例，本文提出的两种算法的求解效率为完备方法的5倍左右.对于CBS类实例，由于采样的实例的模型数均不低于80，本文提出的两种算法并不具备求解效率上的优势.