基于寻找可满足2-SAT子问题的SAT算法

New SAT solver based on finding satisfiable 2-SAT sub problem

可满足问题(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 FS- SAT. 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.