×

Resolution and linear CNF formulas: improved \((n,3)\)-MaxSAT algorithms. (English) Zbl 1423.68476

Summary: We study techniques for solving the MaxSAT problem on instances in which the variable degree is bounded by 3. The problem is NP-hard. We show how resolution principle can be applied that converts an instance into an equivalent instance in which the CNF formula becomes a linear CNF formula. We then show how more efficient branching strategies can be applied on linear CNF formulas. As applications, we present two algorithms: one of running time \(O^\ast(1.194^k)\) that solves the parameterized version of the problem, and the other of running time \(O^\ast(1.237^n)\) that solves the optimization version of the problem, both significantly improving previous best upper bounds.

MSC:

68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68W40 Analysis of algorithms
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Bansal, N.; Raman, V., Upper bounds for MAXSAT: further improved, (Proc. ISAAC 1999. Proc. ISAAC 1999, Lecture Notes in Comput. Sci., vol. 1741 (1999)), 247-258 · Zbl 0971.68069
[2] Bliznets, I., A new upper bound for \((n, 3)\)-MAX-SAT, J. Math. Sci., 188, 1, 1-6 (2013) · Zbl 1261.68068
[3] Bliznets, I.; Golovnev, A., A new algorithm for parameterized MAX-SAT, (Proc. IPEC 2012. Proc. IPEC 2012, Lecture Notes in Comput. Sci., vol. 7537 (2012)), 37-48 · Zbl 1360.68494
[4] Bonet, M. L.; Levy, J.; Manya, F., Resolution for Max-SAT, Artificial Intelligence, 171, 8, 606-618 (2007) · Zbl 1168.68541
[5] Chen, J.; Kanj, I., Improved exact algorithms for Max-SAT, Discrete Appl. Math., 142, 17-27 (2004) · Zbl 1077.68116
[6] Chen, J.; Kanj, I.; Jia, W., Vertex cover: further observations and further improvements, J. Algorithms, 41, 280-301 (2001) · Zbl 1017.68087
[7] Chen, J.; Xu, C.; Wang, J., Dealing with 4-variables by resolution: an improved MaxSAT algorithm, (Proc. WADS 2015. Proc. WADS 2015, Lecture Notes in Comput. Sci., vol. 9214 (2015)), 178-188 · Zbl 1359.68120
[8] Davis, M.; Putnam, H., A computing procedure for quantification theory, J. ACM, 7, 201-215 (1960) · Zbl 0212.34203
[9] Gu, J.; Purdom, P.; Wah, W., Algorithms for the satisfiability (SAT) problem: a survey, (Satisfiability Problem: Theory and Applications. Satisfiability Problem: Theory and Applications, DIMACS Ser. Discrete Math. Theoret. Comput. Sci. (1997), AMS), 19-152 · Zbl 0945.03040
[10] (Hochbaum, D., Approximation Algorithms for NP-Hard problems (1997), PWS Publishing Company: PWS Publishing Company Boston, MA) · Zbl 1368.68010
[11] Impagliazzo, R.; Paturi, R., On the complexity of \(k\)-SAT, J. Comput. System Sci., 62, 367-375 (2001) · Zbl 0990.68079
[12] Kratochvil, J.; Savicky, P.; Tuza, Z., One more occurrence of variables makes satisfiability jump from trivial to NP-complete, SIAM J. Comput., 22, 1, 203-210 (1993) · Zbl 0767.68057
[13] Kulikov, A. S., Automated generation of simplification rules for SAT and MAXSAT, (Proc. SAT 2005 (2005), Springer: Springer Berlin, Heidelberg), 430-436 · Zbl 1128.68469
[14] Porschen, S.; Speckenmeyer, E.; Zhao, X., Linear CNF formulas and satisfiability, Discrete Appl. Math., 157, 5, 1046-1068 (2009) · Zbl 1186.68223
[15] Raman, V.; Ravikumar, B.; Rao, S. S., A simplified NP-complete MAXSAT problem, Inform. Process. Lett., 65, 1, 1-6 (1998) · Zbl 1339.68122
[16] Scheder, D., Unsatisfiable linear CNF formulas are large and complex, (Proc. 27th Intl. Symp. on Theoretical Aspects of Computer Science. Proc. 27th Intl. Symp. on Theoretical Aspects of Computer Science, STACS 2010. Proc. 27th Intl. Symp. on Theoretical Aspects of Computer Science. Proc. 27th Intl. Symp. on Theoretical Aspects of Computer Science, STACS 2010, LIPIcs. Leibniz Int. Proc. Inform., vol. 5 (2010)), 621-630 · Zbl 1230.68116
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.