基于分支回溯的NAE-3SAT问题求解算法  

Solution algorithm for the NAE-3SAT problem based on DPLL

作　　者：谷文祥[1,2] 傅琳璐[1] 周俊萍[1] 姜蕴晖[1] 

机构地区：[1]东北师范大学计算机科学与信息技术学院,吉林长春130117 [2]长春建筑学院基础教学部,吉林长春130607

出　　处：《智能系统学报》2012年第6期506-511,共6页CAAI Transactions on Intelligent Systems

基　　金：国家自然科学基金资助项目(61070084;60803102);中央高校基本科研业务费专项资金资助项目(11QNJJ006);浙江师范大学计算机软件与理论省级重中之重学科开放基金资助项目(ZSDZZZZXK37)

摘　　要：NAESAT问题是可满足性问题的一个重要扩展,在集合分裂、最大割集等NP完全问题中有着重要的应用.针对NAESAT问题的泛化NAE-3SAT问题,提出了一个基于分支回溯的精确算法NAE.算法给出了多种化简规则,这些化简规则很好地提高了算法的时间效率.最后证明了算法在最坏情况下的时间复杂度上界为O(1.618n),其中n为公式中的变量数目.The not-all-equal satisfiability（NAESAT） problem is an important extension of the satisfiability（SAT） problem.It has an important application in many NP-complete problems,such as the SET SPLITTING problem and the MAXCUT problem.An exact algorithm NAE based on Davis-Putnam-Logemann-Loveland（DPLL） for the not-all-equal 3-satisfiability（NAE-3SAT） problem is proposed.In the algorithm some new reduction rules are used to simplify the formula.The reduction rules increase the efficiency of the algorithm.The worst-case upper bound for the algorithm is proved to be O（1.618n）,where n is the number of variables in the formula.

关 键 词：NAESAT NAE-3SAT 时间复杂性 NAE-3SAT问题上界 变量数目 分支回溯 

分 类 号：TP301.6[自动化与计算机技术—计算机系统结构]