Translated abstract: |
Abstract | Language |
---|
Bei dem Boole�schen Erfüllbarkeitsproblem für Formeln in konjunktiver Normalform (KNF), kurz SAT genannt, ist eine KNF Formel gegeben und man muss entscheiden, ob diese Formel eine erfüllende Belegung besitzt. Wie bereits bekannt ist, hat S. Cook in seinem bemerkenswerten Ergebnis von 1971 SAT als das erste authentische Problem für die Klasse NP herauskristallisiert. In dieser Arbeit betrachten wir SAT für eine Teilklasse von KNF, die sogenannten Mixed-Horn-Formeln (MHF). Eine Formel F in MHF besteht aus einem 2-KNF Teil P und einem Horn Teil H. Wir zeigen, dass MHF eine zentrale Rolle in KNF spielt, weil viele prominente Probleme, wie z.B. Feedback Vertex Set, Vertex Cover, Dominating Set und Hitting Set leicht als MHF kodiert werden können. Des Weiteren zeigen wir, dass SAT für einige interessante Teilklassen von MHF NP-vollständig bleibt. Sodann stellen wir Algorithmen für zwei solcher Teilklassen vor, die SAT in einer besseren Laufzeit als O(2^0.5284n) lösen, was soweit die beste Schranke für MHF ist. Eine dieser Teilklassen besteht aus Formeln, bei denen der Horn Teil negativ monoton ist und der zugehörige Variablengraph des entsprechenden positiv monotonen 2-KNF-Teils P nur aus disjunkten Dreiecken besteht. Für die zweite Teilklasse, die aus gewissen k-uniformen, linearen Mixed-Horn-Formeln besteht, geben wir einen Algorithmus an, der SAT in Zeit O(k^(n/ k)) für k>= 4 löst. Zusätzlich betrachten wir Mixed-Horn-Formeln F, für die gilt: H ist negativ monoton, c<=3, für alle c aus H, und P besteht nur aus positiven 2-Klauseln. Wir können SAT in der Laufzeit O(1.325^n) für diese Formelklasse lösen, indem wir das Autarkie-Prinzip benutzen. Das bedeutet, wir erzielen eine bessere Laufzeit als die bisher beste Laufzeit O(p(n)1.427^n) von S.Kottler, M.Kaufmann und C.Sinz für diese Klasse von Mixed-Horn-Formeln. Danach widmen wir uns denjenigen Mixed-Horn-Formeln F in MHF, für die gilt: G_P besteht aus disjunkten Dreiecken, Kanten und isolierten Knoten und H besteht aus Horn Klauseln, die höchstens 3 Literale besitzen, aber nicht notwendigerweise negativ monoton sind. Ferner soll gelten V(P)=V(H). Wir können SAT in der Laufzeit O(1.41^n) für diese Formelklasse lösen, indem wir ebenfalls das Autarkie-Prinzip benutzen. Danach betrachten wir noch einige interessante Teilklassen von MHF, für die wir SAT in Polynomzeit lösen können. Dann präsentieren wir einen Algorithmus, der SAT für Mixed-Horn-Formeln mit einem linearen, negativ monotonen und k-uniformen Horn-Teil und einem P-Teil, bestehend nur aus positiv monotonen und disjunkten 2-Klauseln, löst. Experimentelle Ergebnisse führen zu der starken Vermutung, dass dessen Laufzeit besser ist als O(3^(n/3), wobei n die Anzahl der Variablen einer solchen Formel bezeichnet. Als Nächstes erforschen wir die Komplexität einiger prominenter Varianten von SAT, nämlich NAESAT und XSAT, eingeschränkt auf die Klasse der linearen Formeln. Je zwei Klauseln einer linearen Formel haben höchstens eine Variable gemeinsam. Wir zeigen, dass NAESAT und XSAT für monotone und lineare Formeln, deren Klauseln länger oder gleich k sind, k>= 3, NP-vollständig sind. Ferner beweisen wir, dass XSAT für KNF-Formeln, die l-regulär sind, d.h. in denen jede Variable genau l Mal vorkommt, wobei l>=3 eine feste ganze Zahl ist, NP-vollständig ist. Darauf aufbauend können wir auch die NP-Vollständigkeit von XSAT für die Teilklasse der linearen und l-regulären Formeln zeigen. Dieses Ergebnis ist auch auf den monotonen Fall übertragbar. Ein weiteres Resultat dieser Arbeit ist ein Algorithmus, der XSAT für die Klasse der monotonen, linearen und l-regulären Formeln schneller löst als der bis dato schnellste Algorithmus von J. M. Byskov für KNF-XSAT mit einer Laufzeit von O(2^0.2325n). Indem wir einige Verbindungen zu den projektiven Ebenen nutzen, können wir auch zeigen, dass XSAT NP-vollständig bleibt für die Klasse der linearen und l-regulären Formeln, die zusätzlich l-uniform sind, wobei l=q+1 und q eine Primzahlpotenz ist. Daher ist es sehr wahrscheinlich, dass XSAT auch NP-vollständig ist für alle anderen Werte von l>=3. Wir interessieren uns im Weiteren für die exakt linearen Formeln: Je zwei Klauseln haben hier genau eine Variable gemeinsam. Wir zeigen, dass NAESAT für die Klasse der exakt linearen Formeln in Polynomzeit gelöst werden kann. Wenn wir dieses Ergebnis neu deuten, dann ermöglicht es uns eine teilweise Antwort auf eine lange offen stehende Frage, die von T.Eiter gestellt worden ist: Klassifizieren der Berechnungskomplexität des SIM-UNSAT-Problems. Als Nächstes zeigen wir die NP-Vollständigkeit von XSAT für monotone und exakt lineare Formeln, deren Klauseln mindestens Länge k, k>=3, haben. Dies ist überraschend, da sowohl SAT als auch NAESAT beide in Polynomzeit für exakt lineare Formeln gelöst werden können. Für k=3,4,5,6 können wir jedoch zeigen, dass XSAT für die k-uniformen, monotonen und exakt linearen Formeln in Polynomzeit gelöst werden kann. | German |
|