Exakte Bestimmung von Phasenübergangspunkten in Erfüllbarkeitsproblemen

Bei Erfüllbarkeitsproblemen geht es ganz allgemein darum festzustellen, ob N Variable so eingestellt werden können, daß sie gleichzeitig M Gleichungen erfüllen können. Das klassische Beispiel ist das Satisfiability-Problem (SAT), bei dem die Variablen nur die Werte 0 oder 1 annehmen können, und eine Gleichung, die k Variable enthält, eine Untermenge der 2 hoch k möglichen Belegungen ausschließt. In der Unterhaltungsmathematik sind solche Probleme als "Logeleien" bekannt. In industriellen Anwendungen wie dem Chip-Design oder der Planung von Prozessen tauchen SAT-Probleme mit tausenden von Variablen und Gleichungen auf. Eine fundamentale Bedeutung erhalten Erfüllbarkeitsprobleme dadurch, dass die meisten ihrer Art NP vollständig sind, d.h. sie sind äquivalent zu der großen Klasse kombinatorischer Probleme, deren Lösung leicht zu verifizieren, aber schwer zu finden ist. 
Wählt man die Gleichungen eines Erfüllbarkeitsproblems zufällig aus, so hat das entstehende Problem eine gewisse Wahrscheinlichkeit, lösbar zu sein. Intuitiv erwartet man, dass diese Wahrscheinlichkeit mit der Zunahme der Anzahl von Gleichungen abnimmt. In der Tat findet man für sehr große Probleme einen scharfen Übergang: ist das Verhältnis M/N unterhalb eines kritischen Wertes, so geht die Lösbarkeits-Wahrscheinlichkeit gegen 1 wenn M und N gegen Unendlich gehen. Ist das Verhältnis M/N dagegen größer als dieser kritische Wert, so geht die Lösbarkeits-Wahrscheinlichkeit gegen 0. 
Die Werte für das kritische Verhältnis M/N sind nur für sehr wenige Probleme exakt bekannt. Für die meisten Erfüllbarkeitsprobleme kennt man diese Werte nur näherungsweise aus Simulationen oder durch rigorose, aber auseinander klaffende  untere und obere Schranken. Manche Werte wurden in der Vergangenheit durch sehr mächtige, aber nicht-rigorose Methoden der statistischen Physik bestimmt.
In diesem Projekt geht es darum, die Klasse der Probleme zu erweitern, für die man den kritischen Übergangspunkt exakt bestimmen kann. Das sollte zu einem besseren Verständnis der Komplexität dieser Probleme führen.