中国科学E辑
中國科學E輯
중국과학E집
SCIENCE IN CHINA (SERIES E)
2007年
12期
1597-1606
,共10页
荆明娥%周电%唐璞山%周晓方%张华
荊明娥%週電%唐璞山%週曉方%張華
형명아%주전%당박산%주효방%장화
可满足性问题%DPLL%完全算法%变量决策
可滿足性問題%DPLL%完全算法%變量決策
가만족성문제%DPLL%완전산법%변량결책
提出了一种启发式极性决策的可满足性问题(SAT)新算法. 该算法继承了当前SAT解决器的许多策略: 快速BCP、子句记录、重启动搜索等. 同时, 该算法通过预先根据Karnaugh图的覆盖分布计算变量极性, 将其加入到DPLL的决策过程中, 大大降低了搜索过程中的冲突次数. 实验表明采用该算法的解决器--DiffSat, 能够解决许多目前最有效的解决器Zchaff和MiniSat所不能解决的实例. 尤其是对于Bart基准系列中的每个实例, DiffSat都能够在0.03 s内解决, 而Zchaff和MiniSat在给定的900 s内不能够解决大部分实例. 而且, DiffSat解决器在某些实例上的特性远远优于具有代表性的基于不完全随机算法的解决器DLM.
提齣瞭一種啟髮式極性決策的可滿足性問題(SAT)新算法. 該算法繼承瞭噹前SAT解決器的許多策略: 快速BCP、子句記錄、重啟動搜索等. 同時, 該算法通過預先根據Karnaugh圖的覆蓋分佈計算變量極性, 將其加入到DPLL的決策過程中, 大大降低瞭搜索過程中的遲突次數. 實驗錶明採用該算法的解決器--DiffSat, 能夠解決許多目前最有效的解決器Zchaff和MiniSat所不能解決的實例. 尤其是對于Bart基準繫列中的每箇實例, DiffSat都能夠在0.03 s內解決, 而Zchaff和MiniSat在給定的900 s內不能夠解決大部分實例. 而且, DiffSat解決器在某些實例上的特性遠遠優于具有代錶性的基于不完全隨機算法的解決器DLM.
제출료일충계발식겁성결책적가만족성문제(SAT)신산법. 해산법계승료당전SAT해결기적허다책략: 쾌속BCP、자구기록、중계동수색등. 동시, 해산법통과예선근거Karnaugh도적복개분포계산변량겁성, 장기가입도DPLL적결책과정중, 대대강저료수색과정중적충돌차수. 실험표명채용해산법적해결기--DiffSat, 능구해결허다목전최유효적해결기Zchaff화MiniSat소불능해결적실례. 우기시대우Bart기준계렬중적매개실례, DiffSat도능구재0.03 s내해결, 이Zchaff화MiniSat재급정적900 s내불능구해결대부분실례. 이차, DiffSat해결기재모사실례상적특성원원우우구유대표성적기우불완전수궤산법적해결기DLM.
