# zbMATH — the first resource for mathematics

Solving satisfiability in less than $$2^ n$$ steps. (English) Zbl 0603.68092
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)$$.

##### MSC:
 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) 68Q25 Analysis of algorithms and problem complexity
##### Keywords:
algorithm; boolean formula; conjunctive normal form
Full Text:
##### References:
 [1] Cook, S.A., The complexity of theorem-proving procedures, (), 151-158 · Zbl 0363.68125 [2] Franco, J.; Paull, M., Probabilistic analysis of the Davis-Putnam procedure for solving the satisfiability problem, Discrete appl. math., 5, 77-87, (1983) · Zbl 0497.68021 [3] Goldberg, A., Average case complexity of the satisfiability problem, (), 1-6 [4] Goldberg, A.; Purdom, P.; Brown, C., Average time analyses of simplified Davis-Putnam procedures, Inform. process. lett., 15, 2, 72-75, (1982) · Zbl 0529.68065 [5] Monien, B.; Janssen, D., Über die komplexität der fehlerdiagnose bei systemen, Z. ang. mathem. mech., T315-T317, (1977) · Zbl 0381.03047
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.