Wir beschäftigen uns mit dem Äquivalenztest monotoner
Formeln in Normalform MONET.
Obwohl dieses Problem sehr abstrakt klingt, hat es
Anwendungen in vielen verschiedenen Gebieten.
Wir haben bereits einige Algorithmen implementiert.
Sie sollen nun mit Methoden des Algorithm Engineering verbessert werden.
Datenstrukturen
Die Rechenzeit unserer Implementierungen hängt stark von
der benutzten Datenstruktur ab.
Bereits bei verschiedenen Standard-Datenstrukturen kann man
große Unterschiede in den Rechenzeiten sehen.
Wir sind ständig auf der Suche nach besseren Datenstrukturen.
Heuristiken
Die Algorithmen für MONET suchen mittels unterschiedlicher
Strategien nach Variablen in der Formel, für die die beiden
möglichen Belegungen mit 0 und 1 ausprobiert werden.
Dadurch entstehen neue Formeln, die rekursiv bearbeitet werden.
War die Variable geschickt gewählt, dann
geht die Rekursion nicht zu sehr in die Tiefe.
Wir probieren Heuristiken aus und versuchen, neue und bessere
Heuristiken zu finden.
Logik
Intuitionistische Logik
Intuitionistische Logik ist eine Logik,
die das Gesetz vom ausgeschlossenen Dritten nicht kennt.
Das Erfüllbarkeitsproblem für intuitionistische
Aussagenlogik ist genauso schwer wie für klassische Aussagenlogik (NP-vollständig).
Das Tautologieproblem, das für klassische Aussagenlogik coNP-vollständig ist,
wird für intuitionistische Aussagenlogik jedoch PSPACE-vollständig.
Wir wollen das Model-Checking für intuitionistische Aussagenlogik untersuchen.
Dabei handelt es sich um das Problem, eine Formel für ein gegebenes Modell
auszuwerten.
Wir wissen, dass das Problem in P liegt, und wir wissen auch,
dass es NL-hart ist.
Die Lücke zwischen dieser oberen und der unteren Schranke soll
verkleinert werden.
Intuitionistische hybride Logik
Was passiert, wenn man modale/hybride Logik intuitionisch macht?
Wie sehen solche Logiken aus?
Wie verändert sich die Komplexität des Erfüllbarkeitsproblems?
Multi-Agenten Spiele
Partiell-sichtbare stochastische Spiele
Partiell-sichtbare stochastische Spiele (POSGs) sind ein
Modell für Spiele, bei denen Zufall eine Rolle spielt
und bei denen die Spieler nicht genau wissen, was los ist
(d.h. sie kennen den Zustand des Spiels nicht genau).
Zum Beispiel lässt sich Skat damit modellieren,
oder auch Roboterfußball.
Hat man ein Spiel mit POSGs modelliert, dann möchte man
gerne wissen, ob ein Spieler (oder eine Mannschaft)
eine Gewinnstrategie besitzt.
Wir wissen bereits, dass diese Frage für einen
alleine spielenden Spieler (der sozusagen nur gegen den
Zufall spielt) leichter zu beantworten ist als
für zwei gemeinsam spielende Spieler,
und letzteres ist wiederum leichter als
für zwei Mannschaften aus jeweils zwei Spielern.
Thema dieser Arbeit sind andere Kombinationen
wie z.B. zwei Mannschaften, bei denen eine aus einem
Spieler und die andere aus zwei Spielern besteht usw.
Außerdem beeinflusst die Art der Kommunikation zwischen
den Spielern die Komplexität.
Koalitions-Spiele
Eine zentrale Frage in Koalitions-Spielen ist die
Verteilung der Macht in einer Koalition, die die Mehrheit
gewonnen hat. Wie man es aus der Politik kennt, werden die
Ministerposten in einer Koalitions-Regierung nicht entsprechend
den Stimmenanteilen der Koalitionspartner verteilt.
Wir untersuchen, wie schwierig es ist, eine Machtverteilung zu finden,
unter der Koalitionen besonders stabil sind.
Der Nucleolus ist eine Lösungsstrategie für stabile Koalitions-Spiele.
Modelliert man Koalitions-Spiele als Weighted Graph Games,
dann kann der Nucleolus in FP(NP) berechnet werden.
Wir sind an einem Resultat für die Modellierung als Weighted Threshold Games interessiert.
Ausführliche Informationen zu diesen Themen
gibt es auf Nachfrage.