×

New methods for 3-SAT decision and worst-case analysis. (English) Zbl 0930.68066

Summary: We prove the worst-case upper bound \(1.5045..^{n}\) for the time complexity of 3-SAT decision, where \(n\) is the number of variables in the input formula, introducing new methods for the analysis as well as new algorithmic techniques. We add new 2- and 3-clauses, called “blocked clauses”, generalizing the extension rule of “Extended Resolution.” Our methods for estimating the size of trees lead to a refined measure of formula complexity of 3-clause-sets and can be applied also to arbitrary trees.

MSC:

68Q25 Analysis of algorithms and problem complexity

Software:

DIMACS
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Beigel, R.; Eppstein, D., 3-coloring in time \(O(1.3446^n)\): a no-MIS algorithm, (36th IEEE Symp. on Foundations of Computer Science (1995)), 444-452 · Zbl 0938.68940
[2] Beigel, R.; Floyd, R., The Language of Machines: An Introduction of Computability and Formal Languages (1993), Computer Science Press: Computer Science Press New York
[3] Dantsin, E., Two systems for proving tautologies, based on the split method, J. Sov. Math., 22, 1293-1305 (1983) · Zbl 0509.03004
[4] Davis, M.; Logemann, G.; Loveland, D., A machine program for theorem-proving, Comm. ACM, 5, 394-397 (1962) · Zbl 0217.54002
[5] Davis, M.; Putnam, H., A computing procedure for quantification theory, J. ACM, 7, 201-215 (1960) · Zbl 0212.34203
[6] (Du, D.; Gu, J.; Pardalos, P. M., Satisfiability Problem: Theory and Applications DIMACS Workshop. Satisfiability Problem: Theory and Applications DIMACS Workshop, March 11-13, 1996. Satisfiability Problem: Theory and Applications DIMACS Workshop. Satisfiability Problem: Theory and Applications DIMACS Workshop, March 11-13, 1996, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 35 (1997), American Mathematical Society: American Mathematical Society Providence, RI) · Zbl 0881.00041
[7] (Franco, J.; Gallo, G.; Büning, H.; Speckenmeyer, E.; Spera, C., Workshop on the Satisfiability Problem. Workshop on the Satisfiability Problem, Universität zu Köln, Report No. 96-230 (April 29-May 3 1996)), Siena
[8] Gelder, A. V., A satisfiability tester for non-clausal propositional calculus, Inform. and Comput., 79, 1-21 (1988) · Zbl 0658.68107
[9] Gelder, A. V., Propositional search with \(k\)-clause introduction can be polynomially simulated by resolution, (5th Internat. Symp. on Artificial Intelligence and Mathematics (January 1998))
[10] Gelder, A. V.; Tsuji, Y. K., Satisfiability testing with more reasoning and less guessing, (Johnson, D. S.; Trick, M., Cliques, Coloring, and Satisfiability: Second DIMACS Implementation Challenge DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 26 (1996), American Mathematical Society: American Mathematical Society Providence, RI), 559-586 · Zbl 0868.03007
[11] Gu, J.; Purdom, P. W.; Franco, J.; Wah, B. W., Algorithms for the satisfiability (SAT) problem: A survey, (Du, D.; Gu, J.; Pardalos, P. M., Satisfiability Problem: Theory and Applications DIMACS Workshop. Satisfiability Problem: Theory and Applications DIMACS Workshop, March 11-13, 1996. Satisfiability Problem: Theory and Applications DIMACS Workshop. Satisfiability Problem: Theory and Applications DIMACS Workshop, March 11-13, 1996, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 35 (1997), American Mathematical Society: American Mathematical Society Providence, RI) · Zbl 0945.03040
[12] E. Hirsch, Two new upper bounds for SAT, Proc. SODA’98, to appear.; E. Hirsch, Two new upper bounds for SAT, Proc. SODA’98, to appear. · Zbl 0936.68113
[13] Hooker, J. N.; Vinay, V., Branching rules for satisfiability, J. Autom. Reasoning, 15, 359-383 (1995) · Zbl 0838.68098
[14] Hunt, H. B.; Stearns, R. E., Power indices and easier hard problems, Math. Systems Theory, 23, 209-225 (1990) · Zbl 0719.68025
[15] Krajic̆ek, J., Bounded Arithmetic, Propositional Logic, and Complexity Theory (1995), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0835.03025
[16] Kullmann, O., Methods for 3-SAT-decision in less than \(2^{0.59 · n}\) steps, (Abstracts of contributed papers of the Logic Colloquium’ 93. Abstracts of contributed papers of the Logic Colloquium’ 93, Keele, England, July 20-29, 1993. Abstracts of contributed papers of the Logic Colloquium’ 93. Abstracts of contributed papers of the Logic Colloquium’ 93, Keele, England, July 20-29, 1993, Bull. Symbol. Logic, 1 (1995)), 96-97, (1)
[17] Kullmann, O., A note on a generlization of extended resolution, (Franco, J.; Gallo, G.; Büning, H.; Speckenmeyer, E.; Spera, C., Workshop on the Satisfiability Problem. Workshop on the Satisfiability Problem, Universität zu Köln, Report No. 96-230 (April 29-May 3 1996)), 73-95, Revised: [18]
[18] Kullmann, O., On a generalization of extended resolution, Discrete Appl. Math. (1996), submitted (special edition on the satisfiability problem); revised version of [17] · Zbl 0941.68126
[19] Kullmann, O., Heuristics for SAT algorithms: A systematic study, (SAT’98, Second Workshop on the Satisfiability Problem. SAT’98, Second Workshop on the Satisfiability Problem, May 10-14 (1998)), Eringerfeld, Germany · Zbl 0930.68066
[20] Kullmann, O., Worst-case analysis, 3-SAT decision and lower bounds: approaches for improved SAT algorithms, (Du, D.; Gu, J.; Pardalos, P. M., Satisfiability Problem: Theory and Applications DIMACS Workshop. Satisfiability Problem: Theory and Applications DIMACS Workshop, March 11-13, 1996. Satisfiability Problem: Theory and Applications DIMACS Workshop. Satisfiability Problem: Theory and Applications DIMACS Workshop, March 11-13, 1996, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 35 (1997), American Mathematical Society: American Mathematical Society Providence, RI), 261-313 · Zbl 0889.03030
[21] O. Kullmann, The combination of extended resolution and DPLL-algorithms, forthcoming.; O. Kullmann, The combination of extended resolution and DPLL-algorithms, forthcoming.
[22] O. Kullmann, H. Luckhardt, Deciding propositional tautologies: algorithms and their complexity, Inform. and Comput. submitted.; O. Kullmann, H. Luckhardt, Deciding propositional tautologies: algorithms and their complexity, Inform. and Comput. submitted.
[23] Luckhardt, H., Obere Komplexitätsschranken für TAUT-Entscheidungen, (Frege Conf.. Frege Conf., 1984, Schwerin (1984), Akademie-Verlag: Akademie-Verlag Berlin), 331-337 · Zbl 0592.68041
[24] Monien, B.; Speckenmeyer, E., (3-satisfiability is testable in \(O(1.62^r)\) steps, Technical Report Bericht Nr. 3/1979 (1979), Universität-Gesamthochschule-Paderborn), Reihe Theoretische Informatik
[25] Monien, B.; Speckenmeyer, E., Solving satisfiability in less than \(2^n\) steps, Discrete Appl. Math., 10, 287-295 (1985) · Zbl 0603.68092
[26] Papadimitriou, C. H., Computational Complexity (1994), Addison-Wesley: Addison-Wesley Reading, MA · Zbl 0557.68033
[27] Paturi, R.; Pudlak, P.; Zane, F., Satisfiability coding lemma, (Proc. 38th Annual Symp. Foundations of Computer Science (FOCS 97) (1997)), 566-574
[28] Purdom, P. W., Solving satisfiability with less searching, IEEE Trans. Pattern Anal. Machine Intell., 6, 4, 510-513 (1984) · Zbl 0545.68052
[29] Schiermeyer, I., Solving 3-satisfiability in less than \(1.579^n\) steps, (Selected paper from Computer Science Logic ’92. Selected paper from Computer Science Logic ’92, Lecture Notes Computer Science, vol. 702 (1992), Springer: Springer Berlin), 379-394 · Zbl 0788.68066
[30] Schiermeyer, I., Pure literal look ahead: an \(O(1,497^n) 3\)-satisfiability algorithm, (Franco, J.; Gallo, G.; Büning, H.; Speckenmeyer, E.; Spera, C., Workshop on the Satisfiability Problem. Workshop on the Satisfiability Problem, Universität zu Köln, Report No. 96-230 (1996)), 127-136, Siena, April 29-May 3
[31] Stalmarck, G. M.N., Bulletin 95/26 (June 28, 1995), publication:
[32] Tseitin, G. S., On the complexity of derivation in propositional calculus, (Seminars in Mathematics. V.A. Steklov Mathematical Institute, Leningrad, vol. 8 (1968)), (English translation 1970; A.O. Slisenko (Ed.)) · Zbl 0197.00102
[33] Zhang, W., Number of models and satisfiability of sets of clauses, Theoret. Comput. Sci., 155, 277-288 (1996) · Zbl 0873.68094
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.