基于符号模拟和变量划分的SAT算法
针对SAT算法中回溯次数较多的问题,采用基于符号模拟和变量划分的方法来解决其不足.基于符号模拟和变量划分的SAT算法将一个较大的CNF分解为两个子集,每个子集所包含的变量又划分为两个互不相交的子集,仅对那些无法判断的子集,赋以符号值,从而限定了赋予符号值的变量范围,即可减少算法的回溯次数,又能降低内存占用率.理论及实验结果均证明,该算法是合理且有效的.
SAT、符号模拟、合取范式、变量划分
40
TP301.2;TN707(计算技术、计算机技术)
国家自然科学基金60373113;国家重点基础研究发展计划973计划2004CB318000
2008-07-01(万方平台首次上网日期,不代表论文的发表时间)
共5页
121-125