zbMATH — the first resource for mathematics

Worst-case analysis, 3-SAT decision and lower bounds: Approaches for improved SAT algorithms. (English) Zbl 0889.03030
Du, Dingzhu (ed.) et al., Satisfiability problem: theory and applications. DIMACS workshop, Piscataway, NJ, USA, March 11-13, 1996. Providence, RI: AMS, American Mathematical Society. DIMACS, Ser. Discrete Math. Theor. Comput. Sci. 35, 261-313 (1997).
Summary: New methods for worst-case analysis and (3-)SAT decision are presented. The focus lies on the central ideas leading to the improved bound \(1.5045^n\) for 3-SAT decision ([O. Kullmann, “A systematical approach to 3-SAT-decision, yielding 3-SAT-decision in less than \(1.5045^n\) steps”, submitted to Theor. Comput. Sci.]; \(n\) is the number of variables). The implications for SAT decision in general are discussed and elucidated by a number of hypotheses. In addition an exponential lower bound for a general class of SAT-algorithms is given and the only possibilities to remain under this bound are pointed out.
For the entire collection see [Zbl 0881.00041].

03D15 Complexity of computation (including implicit computational complexity)
68Q25 Analysis of algorithms and problem complexity
03B05 Classical propositional logic
03B35 Mechanization of proofs and logical operations