吉林大学学报(信息科学版)
吉林大學學報(信息科學版)
길림대학학보(신식과학판)
JOURNAL OF JILIN UNIVERSITY(INFORMATION SCIENCE EDITION)
2010年
2期
136-140
,共5页
自动推理%DPLL算法%可满足性
自動推理%DPLL算法%可滿足性
자동추리%DPLL산법%가만족성
在实际应用中通常需要求解对应CNF(Conjunctive Normal Form)公式之间仅相差几个子句的一系列SAT(Satisfiability Problem)问题,但目前绝大多数SAT求解算法都是针对单一SAT问题设计的.为此,基于DPLL提出了nDPLL算法,并在随机问题上对该算法的效率进行测试.实验结果表明,nDPLL算法能一次性求解多个SAT问题,对于特定范围的CNF公式集具有较高的效率,CNF公式集的规模越大、相近因子越高、子句数和变量数的比值越大,则nDPLL算法的效率越高.
在實際應用中通常需要求解對應CNF(Conjunctive Normal Form)公式之間僅相差幾箇子句的一繫列SAT(Satisfiability Problem)問題,但目前絕大多數SAT求解算法都是針對單一SAT問題設計的.為此,基于DPLL提齣瞭nDPLL算法,併在隨機問題上對該算法的效率進行測試.實驗結果錶明,nDPLL算法能一次性求解多箇SAT問題,對于特定範圍的CNF公式集具有較高的效率,CNF公式集的規模越大、相近因子越高、子句數和變量數的比值越大,則nDPLL算法的效率越高.
재실제응용중통상수요구해대응CNF(Conjunctive Normal Form)공식지간부상차궤개자구적일계렬SAT(Satisfiability Problem)문제,단목전절대다수SAT구해산법도시침대단일SAT문제설계적.위차,기우DPLL제출료nDPLL산법,병재수궤문제상대해산법적효솔진행측시.실험결과표명,nDPLL산법능일차성구해다개SAT문제,대우특정범위적CNF공식집구유교고적효솔,CNF공식집적규모월대、상근인자월고、자구수화변량수적비치월대,칙nDPLL산법적효솔월고.
