计算机工程与应用
計算機工程與應用
계산궤공정여응용
COMPUTER ENGINEERING AND APPLICATIONS
2008年
30期
64-67
,共4页
形式验证%等价性验证%布尔可满足性%二叉判决图
形式驗證%等價性驗證%佈爾可滿足性%二扠判決圖
형식험증%등개성험증%포이가만족성%이차판결도
目前提高求解SAT问题完全算法的计算效率问题已成为挑战性研究问题.提出了一种基于启发式分组的SAT完备算法.启发式分组策略将一个全局搜索问题,转为局部搜索问题.并将该策略引入到结合BDD与SAT算法的形式验证中,与一般的启发式SAT算法相比,该算法在求解速度和求解问题的规模等方面都明显地改进了,实验结果表明了该算法的可行性和有效性.
目前提高求解SAT問題完全算法的計算效率問題已成為挑戰性研究問題.提齣瞭一種基于啟髮式分組的SAT完備算法.啟髮式分組策略將一箇全跼搜索問題,轉為跼部搜索問題.併將該策略引入到結閤BDD與SAT算法的形式驗證中,與一般的啟髮式SAT算法相比,該算法在求解速度和求解問題的規模等方麵都明顯地改進瞭,實驗結果錶明瞭該算法的可行性和有效性.
목전제고구해SAT문제완전산법적계산효솔문제이성위도전성연구문제.제출료일충기우계발식분조적SAT완비산법.계발식분조책략장일개전국수색문제,전위국부수색문제.병장해책략인입도결합BDD여SAT산법적형식험증중,여일반적계발식SAT산법상비,해산법재구해속도화구해문제적규모등방면도명현지개진료,실험결과표명료해산법적가행성화유효성.
