Deciding propositional tautologies: Algorithms and their complexity
| Author(s) : | H. Luckhardt O. Kullmann, |
| Publisher : | N/A |
| Publication Date : | 1997 |
| ISSN : | N/A |
| Abstract : | We investigate polynomial reductions and efficient branching rules for algorithms deciding propositional tautologies for DNF and coNP--complete subclasses. Upper bounds on the time complexity are given with exponential part 2 ff\Delta(F) where (F) is one of the measures n(F) = #f variables g, `(F) = #f literal occurrences g and k(F) = #f clauses g. We start with a discussion of variants of the algorithms from [Monien/Speckenmeyer85] and [Luckhardt84] with the known upper bound 2, |