Erfüllbarkeitsprobleme

• Antragsteller: Professor Dr. Heribert Vollmer
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2007 bis 2015
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 33177530

• Erstellungsjahr: 2014

Zusammenfassung der Projektergebnisse

Das Erfüllbarkeitsproblem, also das Berechnungsproblem, von einer gegebenen aussagenlogischen Formel zu entscheiden, ob sie erfüllbar ist, ist das klassische NP-vollständige Problem, dessen Studium die Entwicklung der Komplexitätstheorie in nicht zu unterschätzendem Ausmaß geprägt hat. Bekannterweise erlauben eingeschränkte Formelklassen effiziente Entscheidungsalgorithmen, z. B. die bekannten Horn-Formeln. In diesem Projekt wird die Grenze zwischen algorithmischer Nicht-Handhabbarkeit und effizienter Lösbarkeit für Erfüllbarkeitsprobleme und verwandte algorithmische Fragestellungen in verschiedenen logischen Formalismen genau bestimmt unter besonderer Berücksichtigung einer möglichst genauen komplexitätstheoretischen Klassifizierung der effizienten Fälle, etwa im Hinblick auf Speicherbedarf oder Parallelisierbarkeit. Die zu untersuchenden logischen Formalismen stammen aus dem Bereich der neueren nicht-klassischen Aussagenlogik. Es wurden umfangreiche komplexitätstheoretische Klassifikationen für das Erfüllbarkeitsproblem und das Model-Checking-Problem vorgelegt für die temporalen Logiken CTL, CTL+ und CTL* sowie für die hybriden Logiken, die modale und temporale Logiken um diverse nicht-klassische Konstrukte erweitern. Im Bereich der nicht-monotonen Logiken wurden zentrale Inferenzprobleme klassifiziert für Default-Logik, auto-epistemische Logik, Circumscription und Abduktion. Im Bereich der “Logics for Interaction” wurden verschiedene Varianten der modalen Dependence-Logik untersucht. Methodisch greifen die Untersuchungen auf Mittel der universellen Algebra zurück, insbesondere auf den Post’schen Graphen abgeschlossener Klassen von Boole’schen Funktionen.

Projektbezogene Publikationen (Auswahl)

• The complexity of deciding if a Boolean function can be computed by Boolean circuits over a restricted base. Theory of Computing Systems, 44:82–90, 2009
  H. Vollmer
  
• The complexity of generalized satisfiability for linear temporal logic. Logical Methods in Computer Science, 5(1):1–21, 2009
  M. Bauland, T. Schneider, H. Schnoor, I. Schnoor, and H. Vollmer
  
• Model checking CTL is almost always inherently sequential. Logical Methods in Computer Science, 7(2), 2011
  O. Beyersdorff, A. Meier, M. Mundhenk, T. Schneider, M. Thomas, and H. Vollmer
  
• Proof complexity of propositional default logic. Arch. Math. Log., 50(7-8):727–742, 2011
  O. Beyersdorff, A. Meier, S. Müller, M. Thomas, and H. Vollmer
  
• The tractability of model checking for LTL: The good, the bad, and the ugly fragments. ACM Trans. Comput. Log., 12(2):13, 2011
  M. Bauland, M. Mundhenk, T. Schneider, H. Schnoor, I. Schnoor, and H. Vollmer
  
• Parameterized complexity of weighted satisfiability problems. In Theory and Applications of Satisfiability Testing - SAT 2012, number 7317 in Lecture Notes in Computer Science, pages 341–354. Springer, 2012
  Nadia Creignou and Heribert Vollmer
  
• The complexity of reasoning for fragments of autoepistemic logic. ACM Trans. Comput. Log., 13(2):17, 2012
  N. Creignou, A. Meier, M. Thomas, and H. Vollmer
  
• The complexity of reasoning for fragments of default logic. J. Log. Comput., 22(3):587–604, 2012
  O. Beyersdorff, A. Meier, M. Thomas, and H. Vollmer
  
• Complexity results for modal dependence logic. Studia Logica, 101(2):343–366, 2013
  P. Lohmann and H. Vollmer