[1]谷文祥,姜蕴晖,周俊萍,等.最坏情况下Min-2SAT问题的上界[J].智能系统学报,2012,7(3):241-245.
　GU Wenxiang,JIANG Yunhui,ZHOU Junping,et al.New worstcase upper bounds for Min-2SAT problems[J].CAAI Transactions on Intelligent Systems,2012,7(3):241-245.
点击复制

最坏情况下Min-2SAT问题的上界

《智能系统学报》[ISSN 1673-4785/CN 23-1538/TP] 卷: 7 期数: 2012年第3期 页码: 241-245 栏目: 学术论文—人工智能基础 出版日期: 2012-06-25
Title:
New worstcase upper bounds for Min-2SAT problems
文章编号:
1673-4785(2012)03-0241-05
作者:
谷文祥1,2，姜蕴晖1，周俊萍1，殷明浩1
1.东北师范大学 计算机科学与信息技术学院，吉林 长春 130117；
2.长春建筑学院 基础教学部，吉林 长春 130607
Author(s):
GU Wenxiang1,2, JIANG Yunhui1, ZHOU Junping1, YIN Minghao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
关键词:
MaxSAT; MinSAT; Min2SAT; MaxSAT问题的上界; Min2SAT问题的上界; 子句数目; 分支树
Keywords:
maximum satisfiability;  minimum satisfiability;  minimum twosatisfiability;  upper bounds for maximum satisfiability;  upper bounds for minimum twosatisfiability;  number of clauses;  branching tree
分类号:
TP301
文献标志码:
A
摘要:
最坏情况下MaxSAT问题上界的研究已成为一个热门的研究领域.与MaxSAT问题相对的是MinSAT问题，在求解某些组合优化问题时，将其转化为MinSAT问题比转化为MaxSAT问题有着更快的速度，因此对MinSAT问题进行研究.针对Min2SAT问题提出算法MinSATAlg，该算法首先利用化简算法Simplify对公式进行化简，然后通过分支树的方法对不同情况的子句进行分支.从子句数目的角度分析算法的时间复杂度并证明Min2SAT问题可在O(1.134 3m)时间内求解，对于每个变量至多出现在3个2子句中的情况，得到最坏情况下的上界为O(1.122 5n)，其中n为变量的数目.
Abstract:
The rigorous theoretical analyses of algorithms for solving the upper bounds of maximum satisfiability (MaxSAT) problems have been proposed in research literature. The opposite problem of MaxSAT is the minimum satisfiability (MinSAT) problem. Solving some combinatorial optimization problems by reducing them to MinSAT form may be substantially faster than reducing them to MaxSAT form, so the MinSAT problem was researched in this paper. An algorithm (MinSATAlg) was presented for the minimum twosatisfiability (Min2SAT) problem. In this paper, first, the simplification algorithm Simplify was used for simplification of formulas. Secondly, the branching tree method was used for branching on different kinds of clauses. It was proven that this algorithm can solve the Min2SAT problem in O (1.134 3m), regarding the number of clauses as parameters. The upper bound in the worst case was derived as O(1.122 5n), where n is the number of variables in an input formula for a particular case of Min2SAT in which each variable appears in three 2clauses at most.
参考文献/References:
［1］HANSEN P, JAUMARD B. Algorithms for the maximum satisfiability problem［J］. Computing, 1990, 44(4): 279303.
［2］WALLACE R J. Enhancing maximum satisfiability algorithms with pure literal strategies［C］//Proceedings of the 11th Biennial Conference of the Canadian Society for Computational Studies of Intelligence on Advances in Artificial Intelligence. London, UK: SpringerVerlag, 1996: 388401.
［3］NIEDERMEIER R, ROSSMANITH P. New upper bounds for MaxSat［C］//Proceedings of the 26th International Colloquium on Automata, Languages and Programming. London, UK: SpringerVerlag, 1999: 575584.
［4］GRAMM J, HIRSCH E A, NIEDERMEIER R, et al. Worstcase upper bounds for MAX2SAT with an application to MAXCUT［J］. Discrete Applied Mathematics, 2003, 130(2): 139155.
［5］KNEIS J, ROSSMANITH P. A new satisfiability algorithm with applications to MaxCut: Technical Report AIB200508［R］. Aachen, Germany: Department of Computer Science, RWTH Aachen University, 2005.
［6］KULIKOV A S, KUTZKOV K. New bounds for MAXSAT by clause learning［C］//2nd International Symposium on Computer Science in Russia. Ekaterinburg, Russia, 2007: 194204.
［7］BINKELERAIBLE D, FERNAU H. A new upper bound for Max2SAT: a graphtheoretic approach［J］. Journal of Discrete Algorithms, 2010, 8(4): 388401.
［8］GASPERS S, SORKIN G B. A universally fastest algorithm for Max 2Sat, Max 2CSP, and everything in between［J］. Journal of Computer and System Sciences, 2012, 78(1): 305335.
［9］AVIDOR A, ZWICK U. Approximating MIN 2SAT and MIN 3SAT［J］. Theory of Computing Systems, 2005, 38(3): 329345.
［10］MARATHE M V, RAVI S S. On approximation algorithms for the minimum satisfiability problem［J］. Information Processing Letters, 1996, 58(1): 2329.
［11］LI Chumin, MANYA F, QUAN Zhe, et al. Exact MinSAT solving［C］//Proceedings of the 13th International Conference on Theory and Applications of Satisfiability Testing. Berlin/Heidelberg, Germany: SpringerVerlag, 2010: 363368.
［12］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 the TwentyFourth AAAI Conference on Artificial Intelligence. Atlanta, USA, 2010. 
［13］KOJEVNIKOV A, KULIKOV A S. A new approach to proving upper bounds for MAX2SAT［C］//Proceedings of the Seventeenth Annual ACMSIAM Symposium on Discrete Algorithms. New York, USA: ACM, 2006: 1117.

备注/Memo

收稿日期： 2011-09-06.网络出版日期：2012-05-10.
基金项目：国家自然科学基金资助项目（61070084）；国家自然科学青年基金资助项目（60803102）；中央高校基本科研业务费专项资金资助项目(11QNJJ006).
通信作者：姜蕴晖．E-mail: jiangyh215@nenu.edu.cn.
作者简介：
谷文祥，男，1947年生，教授，博士生导师，主要研究方向为智能规划与规划识别.主持或参与国家自然科学基金项目5项、教育部重点项目2项、省科委项目1项.发表学术论文130余篇，出版专著《智能规划与规划识别》，2011年获得吉林省专著类一等奖.
姜蕴晖，女，1987年生，硕士研究生，主要研究方向为智能规划与自动推理.
周俊萍，女，1981年生，讲师，主要研究方向为智能规划与自动推理，发表学术论文5篇.

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