×

zbMATH — the first resource for mathematics

On a generalization of extended resolution. (English) Zbl 0941.68126
Summary: Motivated by improved SAT algorithms yielding new worst-case upper bounds a natural parameterized generalization GER of Extended Resolution (ER) is introduced. ER can simulate polynomially GER, but GER allows special cases for which exponential lower bounds can be proven.

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] P. Beame, T. Pitassi, Simplified and improved resolution lower bounds, In Thirtyseven Symposium on Foundations of Computer Science (FOCS’ 96), 1996, pp. 274-282.
[2] S.A. Cook, A short proof of the pigeonhole principle using extended resolution, SIGACT News, October-December 1976, pp. 28-32.
[3] Cook, S.A.; Pitassi, T., A feasibly constructive lower bound for resolution proofs, Inform. process. lett., 34, 81-85, (1990) · Zbl 0702.68065
[4] S.A. Cook, R.A. Reckhow, Corrections for “On the lengths of proofs in the propositional calculus Preliminary version”, SIGACT News 6 (1974) 15-22. Reference: [5]. · Zbl 0375.02004
[5] S.A. Cook, R.A. Reckhow, On the lengths of proofs in the propositional calculus, In sixth ACM Symposium on the Theory of Computing, May 1974, pp. 135-148. Preliminary version. · Zbl 0375.02004
[6] Cook, S.A.; Reckhow, R.A., The relative efficiency of propositional proof systems, J. symbolic logic, 44, 1, 36-50, (1979) · Zbl 0408.03044
[7] J. Franco, G. Gallo, H.K. Büning, E. Speckenmeyer, C. Spera (Eds.), Workshop on the Satisfiability Problem. Universität zu Köln, Report No. 96-230, 1996. Siena, 29 April - 3 May 1996.
[8] Haken, A., The intractability of resolution, Theoret. comput. sci., 39, 297-308, (1985) · Zbl 0586.03010
[9] Krajiček, J.; Pudlák, P., Propositional proof systems, the consistency of first order theories and the complexity of computations, J. symbolic logic, 54, 3, 1063-1079, (1989) · Zbl 0696.03029
[10] O. Kullmann, Obere und untere Schranken für die Komplexität von aussagenlogischen Resolutionsbeweisen und Klassen von SAT-Algorithmen. Master’s thesis, Johann Wolfgang Goethe-Universität Frankfurt am Main, April 1992. (Upper and lower bounds for the complexity of propositional resolution proofs and classes of SAT algorithms (German)).
[11] O. Kullmann, An exponential lower bound for a general class of DPLL-like algorithms for SAT-decision, Preprint, March 1996.
[12] O. Kullmann, A note on a generalization of extended resolution, in: Franco et al. [7], pages 73-95. Siena, April 29 - May 3 (1996).
[13] O. Kullmann, Worst-case analysis, 3-SAT decision and lower bounds: Approaches for improved SAT algorithms. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 35, American Mathematical Society, Providence, RI, 1997, 261-313. · Zbl 0889.03030
[14] O. Kullmann, New methods for 3-SAT decision and worst-case analysis, Theoret. Comput. Sci., 1999. · Zbl 0930.68066
[15] O. Kullmann, H. Luckhardt, Deciding propositional tautologies: algorithms and their complexity, Inform. Comput., Technical report (http://mi.informatik.uni-frankfurt.de/people/kullmann.kullmann.html). Improved version “Algorithms for SAT/TAUT decision based on various measures”, submitted to Information and Computation.
[16] H. Luckhardt, Obere Komplexitätsschranken für TAUT-Entscheidungen, Frege Conference 1984, Schwerin, Akademie-Verlag, Berlin, 1984, pp. 331-337.
[17] Monien, B.; Speckenmeyer, E., Solving satisfiability in less than 2^{n} steps, Discrete app. math., 10, 287-295, (1985) · Zbl 0603.68092
[18] Purdom, P.W., Solving satisfiability with less searching, IEEE trans. on pattern anal. Mach. intell., 6, 4, 510-513, (1984) · Zbl 0545.68052
[19] I. Schiermeyer, Pure literal look ahead: An O(1,497^{n}) 3-satisfiability algorithm, in: Franco et al. [7], pages 127-136. Siena, April 29-May 3 (1996).
[20] U. Schöning, Perlen der theoretischen Informatik, BI-Wissenschaftsverlag, 1995.
[21] G.S. Tseitin, On the complexity of derivation in propositional calculus, in: A.O. Slisenko (Ed.), Seminars in Mathematics, vol. 8. V.A. Steklov Mathematical Institute, Leningrad, 1968. English translation: Studies in Mathematics and Mathematical logic, Part II, 1970, pp. 115-125. · Zbl 0197.00102
[22] Urquhart, A., The complexity of propositional proofs, Bull. symbolic logic, 1, 4, 425-467, (1995) · Zbl 0845.03025
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.