Minimal unsatisfiable formulas: structure and algorithms

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

Das Projekt befaßt sich mit minimal unerfüllbaren Formeln der Aussagenlogik, die in konjunktiver Normalform vorliegen. Minimal unerfüllbare Formeln, als Kern jeder unerfüllbaren Formel, spielen eine besondere Rolle bei der Analyse der Leistungsfähigkeit von Erfüllbarkeits- bzw. Deduktionsalgorithmen. Die Menge der minimal unerfüllbaren Formeln mit n + k Klauseln und n Variablen wird mit MU(k) bzeichnet. Das Ziel des Projektes ist es, für festes k die Struktur von Formeln aus Mu(k) zu bestimmen, d.h. eine Charakterisierung zu finden, Entscheidungsalgorithmen für Mu(k) zu entwickeln und aufbauend auf diese Kenntnisse neue untere und obere Schranken für Resolutionsalgorithmen zu beweisen.