Minimal unerfüllbare logische Formeln: Struktur und Algorithmen

• Antragsteller: Professor Dr. Hans Kleine Büning
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 1999 bis 2002
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 5160944

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.

• DFG-Verfahren: Sachbeihilfen
• Internationaler Bezug: China, Russische Föderation, USA
• Beteiligte Personen: Professorin Dr. Inna Davydova; Professor Dr. Ding Decheng; Professor Dr.-Ing. John Franco