×

zbMATH — the first resource for mathematics

Obere Komplexitätsschranken für TAUT-Entscheidungen. (German) Zbl 0592.68041
Frege conference, Proc. Int. Conf., Schwerin/Ger. 1984, Math. Res. 20, 331-337 (1984).
[For the entire collection see Zbl 0544.00005.]
Zunächst werden Transformationen auf disjunktive Normalformen mittels neuer Variablen behandelt, die TAUT respektieren und lineare Komplexität haben. Sie führen auf DNF-Formelnklassen mit asymmetrischer Anzahl (1,2) bzw. (1,m) der Literale und Klauselnlängen \(\geq 3\). Da 2-TAUT und DNF-Formeln, deren Literale nur einmal vorkommen, schnell TAUT-entscheidbar sind, ist diese Asymmetrie wesentlich. Gleichzeitig zeigt sich, daß die Klauselnanzahl im Vergleich zur Variablenanzahl kein stabiles Merkmal ist.
Dann werden zwei TAUT-Algorithmen \(T_ 1\), \(T_ 2\) mit polynomialer Raumkomplexität und einer Zeitkomplexität \(T(i)=P(| i|)\cdot 2^{h\cdot n}\) \((i=input\), P Polynom, \(0\leq h\leq 1\), \(n=Variablenanzahl)\) oder kurz \(T(n)=O(2^{h\cdot n})\) angegeben, die auf ausgesuchten Test-Reduktionen beruhen. Die Testbäume werden in einer kombinatorischen Normalform auf ihren Aufwand hin abgeschätzt. Diese Algorithmen operieren auf verschiedenen DNF-Formelnklassen, auf die sich alle Formeln leicht reduzieren lassen. Bestimmt wird der Exponentenfaktor h bzw. h(p) in Abhängigkeit von der Klauselnlänge \(\leq p\) (p\(\geq 3)\). \(T_ 1\) operiert auf disjunktiven Normalformen (und Verwandten); hier strebt h(p) von 0,6943 ab asymptotisch gegen 1. Dagegen operiert \(T_ 2\) auf disjunktiven Normalformen, in denen für jede Variable jedes ihrer Literale genau einmal auftritt. Hier ist h im schlimmsten Fall \((p=3)\) 0,5286, und h(p) geht für Formeln, deren Klauseln alle die Länge p haben, von da ab gegen 0. Die Klauselnlänge ist also auch kein stabiles einfaches Merkmal.

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