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

New worstcase upper bounds for Min-2SAT problems

CAAI Transactions on Intelligent Systems[ISSN 1673-4785/CN 23-1538/TP] Volume: 7 Number of periods: 2012 3 Page number: 241-245 Column: 学术论文—人工智能基础 Public date: 2012-06-25
Title:
New worstcase upper bounds for Min-2SAT problems
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
Keywords:
maximum satisfiability;  minimum satisfiability;  minimum twosatisfiability;  upper bounds for maximum satisfiability;  upper bounds for minimum twosatisfiability;  number of clauses;  branching tree
CLC:
TP301
DOI:
-
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.
Similar References:

Memo

-

Last Update: 2012-09-05

Copyright © CAAI Transactions on Intelligent Systems