Minimal unsatisfiable formulas: structure and algorithms

• Applicant: Professor Dr. Hans Kleine Büning
• Subject Area: Theoretical Computer Science
• Term: from 1999 to 2002
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 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 Programme: Research Grants
• International Connection: China, Russia, USA
• Participating Persons: Professorin Dr. Inna Davydova; Professor Dr. Ding Decheng; Professor Dr.-Ing. John Franco