Fachbereich Mathematik & Informatik, Universität Paderborn, Fed. Rep. Germany
Abstract:
In this paper we describe and analyse an algorithm for solving the satisfiability problem. If E is a boolean formula in conjunctive normal form with n variables and r clauses, then we will show that this algorithm solves the satisfiability problem for formulas with at most k literals per clause in time O(|F|·kn), where k is the greatest number satisfying k = 2−1/kk−1 (in the case of 3-satisfiability 3 = 1,6181).