×

Quasipolynomial algorithms for recognizing the satisfiability and derivability of propositional formulas. (English. Russian original) Zbl 0629.03013

Sov. Math., Dokl. 34, 273-277 (1987); translation from Dokl. Akad. Nauk SSSR 290, 281-286 (1986).
Cases are considered where an exponential general problem can be broken up into subclasses of polynomial complexity. Quasipolynomiality is defined by \(O(| x|^{r(x)})\), where \(| x|\) is the length of the expression for the problem x, and r(x) is its rank. The paper proposes quasipolynomial algorithms to recognize the satisfiability of propositional formulas, and the derivability of formulas in the classical and intuitionistic propositional calculi. Free and flexible classes of implicative normal forms are introduced, too.
Reviewer: E.Knuth

MSC:

03D15 Complexity of computation (including implicit computational complexity)
68Q25 Analysis of algorithms and problem complexity
PDFBibTeX XMLCite