计算机应用研究
計算機應用研究
계산궤응용연구
APPLICATION RESEARCH OF COMPUTERS
2010年
2期
462-464
,共3页
SAT问题%2-SAT子问题%2-SAT算法
SAT問題%2-SAT子問題%2-SAT算法
SAT문제%2-SAT자문제%2-SAT산법
SAT problem%2-SAT sub problem%2-SAT solver
可满足问题(SAT)是一个NP-Hard问题.提出了一种求解SAT的新算法(FFSAT).该算法将SAT问题转换为寻找一个可满足的2-SAT子问题.SAT问题虽然是NP完全问题,但是当所有子句长度不大于2时,SAT问题可以在线性时间求解.使用2-SAT算法-BinSat求解2-SAT子问题,当它不满足时,根据赋值选择新的2-SAT子问题.实验结果表明,采用本算法的结果优于UnitWalk.
可滿足問題(SAT)是一箇NP-Hard問題.提齣瞭一種求解SAT的新算法(FFSAT).該算法將SAT問題轉換為尋找一箇可滿足的2-SAT子問題.SAT問題雖然是NP完全問題,但是噹所有子句長度不大于2時,SAT問題可以在線性時間求解.使用2-SAT算法-BinSat求解2-SAT子問題,噹它不滿足時,根據賦值選擇新的2-SAT子問題.實驗結果錶明,採用本算法的結果優于UnitWalk.
가만족문제(SAT)시일개NP-Hard문제.제출료일충구해SAT적신산법(FFSAT).해산법장SAT문제전환위심조일개가만족적2-SAT자문제.SAT문제수연시NP완전문제,단시당소유자구장도불대우2시,SAT문제가이재선성시간구해.사용2-SAT산법-BinSat구해2-SAT자문제,당타불만족시,근거부치선택신적2-SAT자문제.실험결과표명,채용본산법적결과우우UnitWalk.
Satisfiability (SAT) problem is one of the NP-Hard problems.This paper introduced a new SAT solver called FSSAT.This SAT solver solved the problem by searching a satisfiable 2-SAT sub problem.SAT was NP-complete,but it can be solved in linear time when the given formula contains only binary clauses (2-SAT).BinSat(2-SAT solver) was used to solve the 2-SAT sub problem and improved the 2-SAT sub problem according to the truth assignment.The experimental results show that the solver outperforms UnitWalk.
