Kombinatorik und (parallele) Algorithmik/Komplexitätstheorie von SAT auf KNF-Teilklassen, insbesondere gemischte Hornformeln

点击翻译按钮获取中文摘要

Im beantragten Projekt sollen komplexitätstheoretische Untersuchungen und daraus folgende Algorithmenentwicklungen zum propositionalen Erfüllbarkeitsproblem der Logik (SAT) vorgenommen werden, das wegen seiner herausragenden Bedeutung auch schon als Drosophila der Komplexitätstheorie bezeichnet worden ist. Im Zentrum der Untersuchungen steht dabei zum einen die spezielle Klasse von Booleschen Formeln, die aus einem quadratischen - und einem Horn-Formelteil bestehen, Mixed Horn Formula (MHF) genannt, siehe [20]. Bei genauerer Untersuchung zeigt sich, dass Reduktionen NP-vollständiger Probleme auf das SAT-Problem in den meisten Fällen MHF's liefern, was sie als zu untersuchende Teilklasse von Formeln besonders attraktiv macht, zumal heute sehr leistungsfähige SAT-Löser verfügar sind, mit deren Hilfe viele NP-vollständige Probleme via Reduktion lösbar sind. Aufbauend auf ersten Strukturresultaten zu MHF's in [20] soll die spezielle Struktur von MHF's weiter untersucht werden, um leistungsfähige SAT-Löser für diese relevante Formelklasse zu entwickeln. Weitere Fragen betreffen obere Laufzeitschranken für MHF's, die wie in [20] gezeigt, beinahe in Zeit 2n/2 lösbar sind, n: Variablenzahl. Eine bessere Laufzeitschranke hätte zur Folge, dass man das allgemeine SAT-Problem in Zeit 2 c.n lösen könnte, für ein c < I ein bis heute offenes Problem. Zum anderen sollen Formeln mit speziellen Hypergraphstrukturen untersucht werden: diese liefern den Schlüssel zum NP-Vollständigkeitsnachweis (etwa im linearen Fall) oder zur Detektion neuer, effizient lösbarer Teilklassen von Formeln. Diese in [22, 21] verfolgten Ansätze sollen weitergetrieben werden. Zusätzlich sollen im weiteren Projektverlauf die Komplexität und Algorithmik von SAT und seiner Varianten bezüglich linearer KNF-Formeln (LKNF) (hier haben die Variablenmengen je zweier verschiedener Klauseln höchstens ein Element gemeinsam) stärker in die Untersuchungen einbezogen werden (vgl. Abschnitt Ziele und Arbeitsprogramm). Der vergleichsweise geringe Überlappungsgrad von Klauseln in linearen Formeln ist vermutlich ursächlich dafür, dass die worstcase Laufzeit aktueller (deterministischer) SAT-Algorithmen und Hitting Set-Algorithmen (auf monotonen Formeln) durch lineare Anteile der Eingangsinstanzen bestimmt werden (10, 6, 16].