计算机辅助设计与图形学学报
計算機輔助設計與圖形學學報
계산궤보조설계여도형학학보
JOURNAL OF COMPUTER-AIDED DESIGN & COMPUTER GRAPHICS
2006年
10期
1472-1477
,共6页
罗二海%荆明娥%尹文波%周电%唐璞山
囉二海%荊明娥%尹文波%週電%唐璞山
라이해%형명아%윤문파%주전%당박산
可满足性问题%DPLL%决策%冲突
可滿足性問題%DPLL%決策%遲突
가만족성문제%DPLL%결책%충돌
采用冲突驱动回溯、两观察变量法等思想,静态分析和动态更新相结合的排序决策,鼓励冲突,尽早剪除不满足解空间,提高算法速度.根据变量正反文字出现次数的乘积进行初始排序,优先考虑正反文字出现次数较多变量的赋值;采用冲突驱动、动态更新变量顺序、优先考虑发生冲突子句中变量的赋值,尽可能避免当前冲突.实验结果表明:与采用其他决策策略的解决器相比,文中的解决器拥有一定的速度优势.
採用遲突驅動迴溯、兩觀察變量法等思想,靜態分析和動態更新相結閤的排序決策,鼓勵遲突,儘早剪除不滿足解空間,提高算法速度.根據變量正反文字齣現次數的乘積進行初始排序,優先攷慮正反文字齣現次數較多變量的賦值;採用遲突驅動、動態更新變量順序、優先攷慮髮生遲突子句中變量的賦值,儘可能避免噹前遲突.實驗結果錶明:與採用其他決策策略的解決器相比,文中的解決器擁有一定的速度優勢.
채용충돌구동회소、량관찰변량법등사상,정태분석화동태경신상결합적배서결책,고려충돌,진조전제불만족해공간,제고산법속도.근거변량정반문자출현차수적승적진행초시배서,우선고필정반문자출현차수교다변량적부치;채용충돌구동、동태경신변량순서、우선고필발생충돌자구중변량적부치,진가능피면당전충돌.실험결과표명:여채용기타결책책략적해결기상비,문중적해결기옹유일정적속도우세.
