Solving satisfiability in less than \(2^ n\) steps (Q1082830)

In this paper we describe and analyze 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| \cdot a^ n_ k)\), where \(a_ k\) is the greatest number satisfying \(a_ k=2-1/a_ k^{k-1}\) (in the case of 3-satisfiability \(a_ 3=1,6181)\).