Worst-case analysis, 3-SAT decision, and lower bounds: Approaches for improved SAT algorithms
Oliver Kullmann · DIMACS series in discrete mathematics and theoretical computer science · 1997
. 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 ([Ku96]; n is the number of variables). The implications for SAT decision in general are discussed and elucidated by a number of hypothesis'. 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. In this article the central ideas leading to the improved worst-case upper bound 1:5045 n for 3-SAT decision ([Ku96]) are presented. 1) In nine sections the following subjects are treated: 1. "Gauging of branchings": The " -function" and the concept of a "distance function" is introduced, our main tools for the analysis of SAT algorithms, and, as we propose, also a basis for (complete) practical algorithms. 2. "Estimating the size of arbitrary trees": The " -Lemma" is presented, yielding an upper bound for the number of l...