×

zbMATH — the first resource for mathematics

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
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Beigel, R.; Eppstein, D., 3-coloring in time O(1.3446^n): a no-MIS algorithm, (), 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 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] ()
[7] (), 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, ()
[10] Gelder, A.V.; Tsuji, Y.K., Satisfiability testing with more reasoning and less guessing, (), 559-586 · Zbl 0868.03007
[11] Gu, J.; Purdom, P.W.; Franco, J.; Wah, B.W., Algorithms for the satisfiability (SAT) problem: A survey, () · Zbl 0945.03040
[12] 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 · Zbl 0835.03025
[16] Kullmann, O., Methods for 3-SAT-decision in less than 2^0.59 · n steps, (), 96-97, (1)
[17] Kullmann, O., A note on a generlization of extended resolution, (), 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, (), Eringerfeld, Germany · Zbl 0930.68066
[20] Kullmann, O., Worst-case analysis, 3-SAT decision and lower bounds: approaches for improved SAT algorithms, (), 261-313 · Zbl 0889.03030
[21] 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.
[23] Luckhardt, H., Obere komplexitätsschranken für TAUT-entscheidungen, (), 331-337 · Zbl 0592.68041
[24] Monien, B.; Speckenmeyer, E., (), 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 Reading, MA · Zbl 0557.68033
[27] Paturi, R.; Pudlak, P.; Zane, F., Satisfiability coding lemma, (), 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, (), 379-394 · Zbl 0788.68066
[30] Schiermeyer, I., Pure literal look ahead: an O(1,497^n) 3-satisfiability algorithm, (), 127-136, Siena, April 29-May 3
[31] Stalmarck, G.M.N.; Stalmarck, G.M.N.; Stalmarck, G.M.N., Method and apparatus for checking propositional logic theorems in system analysis, Bulletin 90/51, Bulletin 95/26, (June 28, 1995), publication:
[32] Tseitin, G.S., On the complexity of derivation in propositional calculus, (), (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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.