Algebraic Techniques for Satisfiability Problems (Tienda española)

Previo

Indice, Datei (35 KB)
Lectura de prueba, Datei (140 KB)

Meine Dissertation besch¨aftigt sich mit verschiedenen Verallgemeinerungen des klas-
sischen Erf¨ullbarkeitsproblems, das in der Komplexit¨atstheorie eine zentrale Rolle spielt.
Durch Erf¨ullbarkeitsprobleme lassen sich viele wichtige Komplexit¨atsklassen charakter-
isieren, und viele offene Fragen der Komplexit¨atstheorie k¨onnen in diesem Kontext for-
muliert werden. Das klassische Erf¨ullbarkeitsproblem ist die Frage, ob eine gegebene
aussagenlogische Formel, in der Variablen sowie die Konnektoren ∧ (und), ∨ (oder) und
¬ (nicht) vorkommem, eine erf¨ullende Belegung hat. Dieses Problem l¨asst sich auf ver-
schiedene Weisen verallgemeinern.
Auf der einen Seite kann man die oben genannten Konnektoren durch beliebige
Kombinationen von Boole’schen Funktionen ersetzen. F¨ur viele dieser eingeschr¨ankten
Klassen kann man zeigen, dass das Erf¨ullbarkeitsproblem und andere interessante Pro-
bleme im Formelkontext effiziente L¨osungen besitzen. In dieser Arbeit werden zwei
wichtige Probleme f¨ur diese Formeln betrachtet: das Formula Value Problem ist die
Frage, ob eine gegebene variablenfreie Formel zu 0 oder zu 1 evaluiert. Dieses Problem
spielt eine zentrale Rolle in vielen Algorithmen, die zur L¨osung von Formelproblemen
eingesetzt werden. Weiterhin wird die Komplexit¨at des Problems, zu einer gegebenen
Formel die Menge ihrer erf¨ullenden Belegungen zu berechnen, klassifiziert.
Auf der anderen Seite betrachtet man Formeln in konjunktiver Normalform. Hier-
bei beschreiben die Formeln eine Menge von Klauseln in einfacher Form, die simultan
erf¨ullt sein m¨ussen. Klassische Vertreter von Problemen in diesem Kontext sind 3SAT
oder 2SAT, wo die Klauseln aus Disjunktionen von maximal 2 bzw. 3 Literalen beste-
hen. Auch hier kann man verallgemeinerte Klauseln betrachten, die beliebige Relatio-
nen zulassen. Solche Probleme werden als Constraint Satisfaction Problems bezeich-
net. F¨ur den Boole’schen Fall wurde die Komplexit¨at dieser Probleme von Thomas
Schaefer im Jahr 1978 betrachtet und er zeigte, dass solche Probleme entweder effizient
l¨osbar oder bereits NP-vollst¨andig sind. In dieser Arbeit wird dieses “Dichotomie”-
Resultat auf verschiedene Weisen verallgemeinert. F¨ur das Boole’sche Problem wird
eine vollst¨andige Klassifizierung der effizienten F¨alle erzielt, und es zeigt sich, dass die
Dichotomie-Eigenschaft, dass also nur eine endliche Menge von “Komplexit¨atsgraden”
angenommen wird, auch hier gilt. Weiterhin wird die Verallgemeinerung des quan-
tifizierten Problems betrachtet, wo in den Formeln zus¨atzlich die Quantoren ∃ und ∀
auftreten. F¨ur diese Formeln werden Erf¨ullbarkeitsprobleme, Z¨ahlprobleme und die
Komplexit¨at des ¨Aquivalenzproblems untersucht. Auch hier ergeben sich dichotomie-
artige Resultate: die Probleme sind effizient l¨osbar oder vollst¨andig f¨ur Stufen in der
Polynomialzeit-Hierarchie.
Die wichtigste Technik, um komplexit¨atstheoterische Ergebnisse f¨ur diese Probleme zu
erzielen, ist die Anwendung von verschiedenen algebraischen Abschlussoperatoren auf der
Menge der Funktionen und der Relationen. Insbesondere existiert eine Galois-Verbindung
zwischen diesen beiden “Welten”, die es erlaubt, Resultate zu ¨ubertragen. Eine wichtige
Frage in der Arbeit ist daher auch die nach den Grenzen der Anwendbarkeit dieses alge-
braischen Ansatzes.