[1]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.
Copy

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

CAAI Transactions on Intelligent Systems[ISSN 1673-4785/CN 23-1538/TP] Volume: 7 Number of periods: 2012 6 Page number: 506-511 Column: 学术论文—智能系统 Public date: 2012-12-25
Title:
Solution algorithm for the NAE3SAT problem based on DPLL
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
Keywords:
notallequal satisfiability;  notallequal 3satisfiability;  time complexity;  upper bounds for NotAllEqual 3satisfiability;  number of variables;  DPLL
CLC:
TP301
DOI:
-
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.
Similar References:

Memo

-

Last Update: 2013-03-19

Copyright © CAAI Transactions on Intelligent Systems