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

摘要

可满足问题(SAT)是一个NP-Hard问题.提出了一种求解SAT的新算法(FFSAT).该算法将SAT问题转换为寻找一个可满足的2-SAT子问题.SAT问题虽然是NP完全问题,但是当所有子句长度不大于2时,SAT问题可以在线性时间求解.使用2-SAT算法-BinSat求解2-SAT子问题,当它不满足时,根据赋值选择新的2-SAT子问题.实验结果表明,采用本算法的结果优于UnitWalk.