[1]谷文祥,傅琳璐,周俊萍,等.基于分支回溯的NAE-3SAT问题求解算法[J].智能系统学报,2012,7(6):506-511.
　GU Wenxiang,FU Linlu,ZHOU Junping,et al.Solution algorithm for the NAE3SAT problem based on DPLL[J].CAAI Transactions on Intelligent Systems,2012,7(6):506-511.
点击复制

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

《智能系统学报》[ISSN 1673-4785/CN 23-1538/TP] 卷: 7 期数: 2012年第6期 页码: 506-511 栏目: 学术论文—智能系统 出版日期: 2012-12-25
Title:
Solution algorithm for the NAE3SAT problem based on DPLL
文章编号:
1673-4785(2012)06-0506-06
作者:
谷文祥1,2，傅琳璐1，周俊萍1，姜蕴晖1
1.东北师范大学 计算机科学与信息技术学院，吉林 长春 130117；
2.长春建筑学院 基础教学部，吉林 长春130607
Author(s):
GU Wenxiang 1,2, FU Linlu 1, ZHOU Junping 1, JIANG Yunhui 1
1. School of Computer Science and Information Technology, Northeast Normal University, Changchun 130117, China;
2. Department of Basic Subjects Teaching, Changchun Architecture & Civil Engineering College, Changchun 130607, China
关键词:
NAESAT; NAE3SAT; 时间复杂性; NAE3SAT问题上界; 变量数目; 分支回溯
Keywords:
notallequal satisfiability;  notallequal 3satisfiability;  time complexity;  upper bounds for NotAllEqual 3satisfiability;  number of variables;  DPLL
分类号:
TP301
文献标志码:
A
摘要:
NAESAT问题是可满足性问题的一个重要扩展，在集合分裂、最大割集等NP完全问题中有着重要的应用．针对NAESAT问题的泛化NAE-3SAT问题,提出了一个基于分支回溯的精确算法NAE．算法给出了多种化简规则，这些化简规则很好地提高了算法的时间效率．最后证明了算法在最坏情况下的时间复杂度上界为O(1.618n)，其中n为公式中的变量数目．
Abstract:
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.618n), where n is the number of variables in the formula.
参考文献/References:
［1］COLMERAUER A. Opening the Prolog III universe［J］. Byte Magazine, 1987, 12(9): 177182.
［2］KLEER J. Exploiting locality in a TMS［C］//Proceedings of the 8th National Conference on Artificial Intelligence. Boston, USA, 1990: 264275.
［3］GU J. Local search for satisfiability (SAT) problem［J］. IEEE Transactions on Systems, Man and Cybernetics, 1993, 23(4): 11081129.
［4］李未, 黄文奇. 一种求解合取范式可满足性问题的数学物理方法［J］. 中国科学: A辑, 1994, 24(11): 12081217. 
LI Wei, HUANG Wenqi. A mathematic physical approach to the satisfiability problems［J］. Science in China： Series A, 1994, 24(11): 12081217.
［5］COOK S A. The complexity of the theoremproving procedures［C］//Proceedings of the Third Annual ACM Symposium on Theory of Computing. New York, USA, 1971: 151158.
［6］MONIEN B, SPECKENMEYER E. Upper bounds for covering problems［R］. UniversitatGesamtho Chschule Paderborn: Reihe Theoretische Informatik, 1980.
［7］HIRSCH E A. New worstcase upper bounds for SAT［J］. Journal of Automated Reasoning, 2000, 24(4): 397420.
［8］YAMAMOTO M. An improved O(1.234m)time deterministic algorithm for SAT［J］. Lecture Notes in Computer Science, 2005, 3827: 644653.
［9］MONIEN B, SPECKENMEYER E. Solving satisfiability in less than 2n steps［J］. Discrete Applied Mathematics, 1985, 10(3): 287295.
［10］BRUEGGEMANN T, KERN W. An improved local search algorithm for 3SAT［J］. Theoretical Computer Science, 2004, 329(1/2/3): 303313.
［11］DANTSIN E, GOERDT A, HIRSCH E A, et al. Adeterministic (22/(k+1))n algorithm for kSAT based on local search［J］. Theoretical Computer Science, 2002, 289(1): 6983.
［12］ZHANG Lintao, MADIGN C F, MOSKEWICZ M H, et al. Efficient conflict driven learning in a Boolean satisfiability solver［C］//Proc of the ACM/IEEE ICCAD 2001. New York, USA, 2001: 279285.
［13］ZECCHINA R, MEZARD M, PARISI G. Analytic and algorithmic solution of random satisfiability problems［J］. Science, 2002, 297(5582): 812815.
［14］ZECCHINA R, MONASSON R, KIRKPATRICK S, et al. Determining computational complexity from characteristic phase transitions［J］. Nature, 1999, 400(6740): 133137.
［15］THOMAS J S. The complexity of satisfiability problems［C］//Conference Record of the Tenth Annual ACM Symposium on Theory of Computing. New York, USA, 1978: 216226.
［16］PORSCHEN S, RANDERATH B, SPECKENMEYER E. Linear time algorithms for some notallequal satisfiability problems［C］//Proceedings of the 6th International Conference on Theory and Application of Satisfiability Testing(SAT2003). Santa Margherita Ligure, Italy, 2003: 172187.
［17］WALSH T. The interface between P and NP: COL, XOR, NAE, 1ink, and Horn SAT［C］//Eighteenth National Conference on Artificial Intelligencet. Edmonton, Canada, 2002: 685700.
［18］MONIEN B, SPECKENMEYER E, VORNBERGER O. Upper bounds for covering problems［J］. Methods of Operations Research, 1981, 43: 419431.
［19］RIEGE T, ROTHE J, SPAKOWSKI H. An improved exact algorithm for the domatic number problem［J］. Information Processing Letters, 2006, 101(3): 101106.
［20］SHI Nungyue, CHU Chihping. A DNAbased algorithm for the solution of notallequal 3SAT problem［C］//ASE International Conference on Information Engineering.Taiyuan, China, 2009: 9497.
［21］ZHOU Junping, YIN Minghao, ZHOU Chunguang. New worstcase upper bound for #2SAT and #3SAT with the number of clauses as the parameter［C］//Proceedings of 24rd AAAI Conference on Artificial Intelligence. Atlanta, USA, 2010: 217222.
［22］周俊萍, 殷明浩, 周春光, 等. 最坏情况下#3SAT问题最小上界［J］. 计算机研究与发展, 2011, 48(11): 20552063. 
ZHOU Junping, YIN Minghao, ZHOU Chunguang, et al. The worst case minimized upper bound in #3SAT［J］. Journal of Computer Research and Development, 2011, 48(11): 20552063.

备注/Memo

收稿日期： 2012-06-08.
网络出版日期：2012-11-16
基金项目：国家自然科学基金资助项目(61070084,60803102)；中央高校基本科研业务费专项资金资助项目(11QNJJ006)；浙江师范大学计算机软件与理论省级重中之重学科开放基金资助项目(ZSDZZZZXK37).
通信作者：傅琳璐.
 E-mail：full820@nenu.edu.cn.
作者简介：
谷文祥，男，1947年生，教授，博士生导师，主要研究方向为智能规划与规划识别、形式语言与自动机、模糊数学及其应用．主持国家自然科学基金项目3项，发表学术论文100余篇． 
傅琳璐，女，1988年生，硕士研究生，主要研究方向为自动推理和智能规划． 
周俊萍，女，1981年生，讲师，博士，主要研究方向为自动推理和智能规划，主持东北师范大学青年基金项目1项，发表学术论文10篇．

更新日期/Last Update: 2013-03-19
Copyright © 《 智能系统学报》 编辑部
地址：（150001）黑龙江省哈尔滨市南岗区南通大街145-1号楼 电话：0451- 82534001、82518134　邮箱：tis@vip.sina.com