Außerdem soll die relative Komplexität von eingeschränkten Formen des Resolutionskalküls untersucht werden. Dabei sollen insbesondere solche Einschränkungen betrachtet werden, die in Anwendungen, etwa in automatischen Theorembeweisern oder in Erfüllbarkeitsalgorithmen, verwendet werden, beispielsweise negative/positive Resolution, reguläre und Davis-Putnam-Resolution oder lineare Resolution.
Der erste Durchbruch kam mit der Arbeit von Razborov [25], in der superpolynomiale untere Schranken an die Größe monotoner Schaltkreise für das Clique-Problem gegeben wurden. Diese wurden von Alon und Boppana [1] zu exponentiellen verbessert, und schließlich gelang Tardos [29] die exponentielle Trennung der Größenkomplexität monotoner und nicht-monotoner boolescher Schaltkreise.
Karchmer und Wigderson [17] geben scharfe untere Schranken der Form log2 n an die Tiefe monotoner boolescher Schaltkreise, die das Problem st-Connectivity berechnen. Diese wurden von Grigni und Sipser [14] auf Schaltkreise mit semi-unbeschränktem Eingangsgrad, in denen die UND-Gatter beliebig viele, die ODER-Gatter jedoch nur zwei Inputs haben dürfen, verallgemeinert. Lineare untere Schranken an die Tiefe von Schaltkreisen zur Berechnung des Matching-Problems wurden von Raz und Wigderson [25] gegeben. Schließlich zeigten Raz und McKenzie [24] untere Schranken der Form ne, für ein geeignetes e>0, an die Tiefe monotoner Schaltkreise für ein Problem Gen, das durch monotone Schaltkreise polynomialer Größe berechenbar ist. Die Beweise aller dieser Tiefenschranken beruhen auf unteren Schranken an die Kommunikationskomplexität eines mit einer monotonen booleschen Funktion assoziierten Suchproblems, des nach [17] so genannten Karchmer-Wigderson-Spiels. Da für boolesche Schaltkreise die Tiefe proportional zum Logarithmus der Formelgröße ist (das sog. Brent-Spira Theorem), folgen aus diesen Tiefenschranken entsprechend große untere Schranken an die Größe monotoner boolescher Formeln. Insbesondere impliziert das Resultat von [24] eine exponentielle Trennung der Größenkomplexität monotoner Schaltkreise und monotoner Formeln.
Ein anderer erfolgreicher Zweig der Komplexitätstheorie befaßt sich mit der Komplexität von Beweissystemen der Aussagenlogik, insbesondere mit dem Ziel, untere Schranken an die Länge von Beweisen zu zeigen. Neben rein theoretischem Interesse sind diese Untersuchungen auch von der Anwendung, in dem Gebiet des automatischen Theorembeweisens oder für Erfüllbarkeitsalgorithmen, her motiviert. Hier sind besonders der bekannte Resolutionskalkül und eingeschränkte Formen desselben, die in der Praxis meist verwendet werden, von Interesse.
Exponentielle untere Schranken für den vollen Resolutionskalkül wurden zuerst von Haken [15] angegeben. Über die relative Komplexität von Einschränkungen des Resolutionskalküls gibt es verhältnismäßig wenige theoretische Untersuchungen.
Daß baumartige Resolutionsbeweise, also solche, in denen eine einmal hergeleitete Klausel nur einmal als Prämisse einer Resolution verwendet werden kann, superpolynomial länger sein können als allgemeine (im Kontrast zu diesen als dag-artige bezeichnete), ist ein Folklore-resultat, ein Beweis findet sich etwa in Urquhart [30]. Reguläre Resolutionsbeweise sind solche, in denen in jedem Pfad durch den Beweis nur einmal nach jeder Variablen resolviert werden darf, und Davis-Putnam-Resolutionen unterliegen der weiteren Einschränkung, daß die Reihenfolge der resolvierten Variablen auf jedem Pfad die Gleiche ist. Von Goerdt [10],[12] wurde gezeigt, daß diese Einschränkungen eine superpolynomiale Beweisverlängerung erzwingen können. Das Gleiche gilt nach [11] auch für sogenannte negative (oder positive) Resolution, in denen in jedem Resolutionsschritt eine der Prämissen nur negative (bzw. positive) Literale enthalten darf.
Ein anderes Beweissystem, das für uns von Interesse ist, ist das von Cook et al. [8] eingeführte Cutting-Planes-System, abgekürzt CP. Dieses operiert mit linearen Ungleichungen in ganzzahligen Koeffizienten, die Schlußregeln sind u.a. Addition von Ungleichungen und Division durch einen gemeinsamen Teiler aller Koeffizienten. Mittels einer kanonischen Übersetzung von Klauseln in lineare Ungleichungen sieht man, daß dieses System mindestens so stark ist wie der Resolutionskalkül. Auch hier werden baumartige und dag-artige Beweise unterschieden, außerdem werden Teilsysteme betrachtet, die durch Einschränkung an die Größe der verwendeten Koeffizienten gegeben sind.
In jüngster Zeit hat sich gezeigt, daß diese zwei Teilgebiete der Komplexitätstheorie eng miteinander verzahnt sind. Unter günstigen Umständen folgen nämlich aus unteren Schranken an die monotone Schaltkreiskomplexität untere Schranken an die Länge von Beweisen in gewissen Beweissystemen, insbesondere dem Resolutionskalkül oder Cutting-Planes-Systemen. Diese günstigen Umstände liegen vor, wenn das betreffende Beweissystem monotone effektive Interpolation erfüllt.
Ein Beweissystem S erfüllt effektive Interpolation, wenn es zu jeder im System beweisbaren Implikation A(p,q) -> B(p,q) eine Craig-Interpolante C(p) gibt, deren Schaltkreisgröße polynomial beschränkt in der Länge eines kürzesten Beweises für A(p,q) -> B(p,q) in S ist. Weiterhin erfüllt S monotone effektive Interpolation, wenn darüberhinaus C(p) monoton gewählt werden kann in den Fällen, wo die gemeinsamen Variablen p nur positiv in A(p,q) -> B(p,q) vorkommen.
Man kann Tautologien konstruieren, deren Interpolanten das Clique-Problem berechnen, diese erfordern daher exponentiell lange Beweise in jedem Beweissystem, das monotone effektive Interpolation erfüllt, wie Resolution [18] und das Teilsystem CP* von CP, in dem die Koeffizienten polynomial beschränkt sein müssen [5]. Umgekehrt zeigen kurze Beweise dieser Tautologien in einem Beweissystem, daß dieses monotone effektive Interpolation nicht erfüllt. Ähnlich zeigen kurze Beweise für eine andere Familie von Tautologien, deren Interpolanten eine vermutete Einwegfunktion invertieren, daß das Beweissystem (unter einer kryptographischen Schwierigkeitshypothese) effektive Interpolation nicht erfüllt. Dies wurde in einer Folge von Arbeiten ([21],[6],[4]) für eine Reihe von immer schwächeren Beweissystemen durchgeführt.
Eine Schwäche des monotonen Interpolationstheorems für Cutting-Planes Beweissysteme ist, daß die Größe der Interpolanten außer von der Beweisgröße auch von der Größe der vorkommenden Koeffizienten abhängt. Daher folgen exponentielle untere Schranken nur für CP*, und nicht für das volle System CP. Zur Umgehung dieser Schwierigkeit führt Pudlák [22] eine Verallgemeinerung von monotonen Schaltkreisen, die monotonen reellen Schaltkreise, ein. Diese rechnen mit reellen Zahlen, ihre Gatter berechnen beliebige zweistellige, schwach monoton steigende reelle Funktionen. Für das volle System CP gilt auch monotone effektive Interpolation, wobei aber die Interpolanten nun monotone reelle Schaltkreise sind. Außerdem zeigt die Konstruktion, daß die Formelgröße der Interpolante polynomial in der Größe eines kleinsten baumartigen CP-Beweises ist. Somit folgen untere Schranken für baumartige Beweise aus unteren Schranken an die Formelgröße.
Exponentielle untere Schranken an die Größe von monotonen reellen Schaltkreisen, und damit von (dag-artigen) Cutting-Planes-Beweisen, wurden von Pudlák [22], Cook und Haken [7] und Fu [9] angegeben. Rosenbloom [28] zeigt, daß für sogenannte slice-Funktionen monotone reelle Schaltkreise exponentiell kleiner sein können als allgemeine, nicht-monotone boolesche. Andererseits gibt Jukna [16] ein hinreichendes Kriterium dafür an, daß eine Funktion exponentiell große monotone reelle Schaltkreise erfordert, insbesondere trifft dieses auf die von Tardos [29] betrachteten Funktionen zu. Somit ist die Größenkomplexität monotoner reeller und nicht-monotoner boolescher Schaltkreise unvergleichbar.
Von Krajícek [20] wurde ein Beweissystem R(CP) vorgeschlagen, das mit Klauseln (Disjunktionen) von CP-Ungleichungen operiert, und zusätzlich zu den Regeln von CP die Resolutionsregel (Schnittregel) verwendet. Dieses erweitert also CP um gewisse Aspekte der Aussagenlogik, also etwa um die Möglichkeit, Fallunterscheidungen zu treffen.
Für Beweise in diesem System gilt monotone effektive Interpolation, falls in jeder Klausel nur wenige (subpolynomial) Ungleichungen mit kleinen (polynomial beschränkten) Koeffizienten vorkommen [20]. Dies gilt sogar für allgemeinere Systeme, die mit Formeln erster Ordnung in CP-Ungleichungen arbeiten, und die Regeln der vollen Logik erster Ordnung verwenden.
In der Arbeit [19] wurde versucht, die Abhängigkeit von der Größe der Koeffizienten durch Verwendung monotoner reeller Schaltkreise zu beseitigen. Dies ist jedoch nur für baumartige Beweise, in denen jede Klausel bloß eine Ungleichung enthält, gelungen.
Aus dem genannten Resultat aus der Arbeit [b] folgt auch, durch die Angabe von entsprechenden oberen Schranken, eine exponentielle Trennung baumartiger Resolution von regulärer sowie negativer Resolution. Weiterhin wurde eine Modifikation der betrachteten Tautologien angegeben, die eine exponentielle Trennung der Davis-Putnam-Resolution von negativer Resolution bezeugt.
Vage mit den Themen des Projektes hängt auch meine Arbeit [c] zusammen, in der das Resultat von Bonet et al. [6], nach dem sog. TC0-Frege Systeme keine effektive Interpolation erfüllen, auf eine eng mit diesen Systemen verwandte arithmetische Theorie übertragen wird.
Dazu ist es nötig, entsprechende untere Schranken an die Größe monotoner reeller Formeln, und damit lineare oder fast lineare untere Schranken an die Tiefe von monotonen reellen Schaltkreisen, zu zeigen, die eine Funktion berechnen, für die es monotone reelle Schaltkreise polynomialer Größe gibt. Eine solch starke Trennung der Tiefen- und Größenkomplexität ist bislang nicht einmal für monotone boolesche Schaltkreise bekannt.
Untersucht werden soll, ob sich die unteren Schranken für das bereits in [24] und [b] verwendete Problem Gen geeignet verbessern lassen, sowie ob sich derartige untere Schranken an die Tiefe monotoner reeller Schaltkreise für monotone P-vollständige Graphenprobleme wie High Degree Subgraph oder High Connectivity Subgraph zeigen lassen.
Eine Trennung von CP* und CP folgt mittels der Interpolationsmethode, wenn eine konkrete Funktion angegeben werden kann, für die monotone reelle Schaltkreise superpolynomial kleiner sein können als monotone boolesche. Ebenso folgt eine Trennung der baumartigen Teilsysteme von CP* und CP aus der Angabe einer konkreten Trennung der Formelgröße, bzw. Tiefe, monotoner reeller und boolescher Schaltkreise. Beide Trennungen sind zwar bekannt, aber nur durch ein nichtkonstruktives Abzählargument gezeigt [28].
Leider hat sich gezeigt, daß sich die meisten zum Beweis unterer Schranken an die monotone Schaltkreiskomplexität verwendeten Methoden so modifizieren lassen, daß sie auf den Fall monotoner reeller Schaltkreise anwendbar werden. Als erster Schritt soll daher geprüft werden, ob sich weitere Beweismethoden für untere Schranken an die Komplexität monotoner boolescher Schaltkreise, wie etwa die Tiefenschranken für Matching von Raz und Wigderson [25] und für Connectivity von Goldman und Håstad [13], auf den Fall monotoner reeller Schaltkreise verallgemeinern lassen.
Als erster Schritt soll geprüft werden, ob sich die untere Schranke von Raz und McKenzie, analog zur Vorgehensweise in der Arbeit von Grigni und Sipser [14], auf Schaltkreise mit UND-Gattern unbeschränkten Eingangsgrads verallgemeinern läßt, womit co-mSACi < mNCi+1 folgen würde, und ob sich die entsprechende obere Schranke zu mACioder sogar mSACiverbessern läßt. Die übrigen Separationen im Diagramm erfordern voraussichtlich wesentlich neue Ideen.
Ebenso liefert im Falle boolescher Schaltkreise die Kommunikationskomplexität des Karchmer-Wigderson-Spiels eine exakte Charakterisierung der Tiefe, doch die reelle Kommunikationskomplexität ist bloß eine untere Schranke für die Tiefe monotoner reeller Schaltkreise. Eine scharfe Charakterisierung würde unter anderem das oben erwähnte Analogon zum Brent-Spira Theorem für monotone reelle Schaltkreise implizieren.
Eine weitere Frage aus diesem Umfeld ist, ob es eine exakte Charakterisierung der Größe monotoner reeller Schaltkreise durch die Größe und reelle Kommunikationskomplexität von Protokollen, die das Karchmer-Wigderson-Spiel lösen, gibt, analog zu der von Razborov [27] und Krajícek [18] für den booleschen Fall angegebenen. Ebenso wie bei den oberen zwei Problemen ist nur eine Richtung der Äquivalenz bekannt [19].
Während diese Systeme CP außen um Aussagenlogik erweiten, wollen wir auch Systeme betrachten, die CP um Aussagenlogik innen erweitern, in denen also boolesche Formeln für die Variablen in den Ungleichungen substituiert werden. Die Formeln in einem solchen Beweissystem wären also Perzeptronen, eine wohluntersuchte Klasse von Schaltkreisen. Als erstes ist eine genaue Formulierung eines solchen Systems anzugeben. Monotone effektive Interpolation könnte dann für solche Beweise gelten, wenn die booleschen Teilformeln von sehr kleiner Tiefe oder selbst monoton sind.
Bezeichnen wir das System, in dem boolesche Formen konstanter Tiefe (AC0-Formeln) für die Variablen in CP-Ungleichungen substituiert sind, mit CP(AC0), so gilt – unter einer starken Komplexitätshypothese – monotone effektive Interpolation wegen des Ergebnisses von Bonet et al. [4] für CP(AC0) nicht, da dies bereits für Systeme, die nur mit booleschen Formeln konstanter Tiefe operieren (AC0-Frege-Systeme), der Fall ist.
Ein weiteres Ziel ist es, unter einer schwächeren Annahme als der in [4] direkt zu zeigen, daß CP(AC0) keine effektive Interpolation erfüllt. Hierfür wird eine direkte Simulation der TC0-Beweise aus [6] durch CP(AC0) benötigt, analog zur Simulation von TC0-Schaltkreisen durch Perzeptronen von Beigel [2]. Zur Simulation von Beweisen ist allerdings die Beigelsche "top-down"-Konstruktion ungeeignet, es ist also zuerst eine neue "bottom-up" Konstruktion von Perzeptronen, die allgemeine TC0-Schaltkreise simulieren, zu finden.
Schließlich betrachtet Pudlák [23] eine Erweiterung von CP durch gewisse quadratische Ungleichungen und Regeln zum Operieren mit diesen, den sogenannten Lovász-Schrijver-Kalkül. Monotone effektive Interpolation durch monotone reelle Schaltkreise gilt für diesen Kalkül, falls es monotone reelle Schaltkreise zur Lösung einer bestimmten Form von linearer Programmierung gibt. Es soll versucht werden, zu klären, ob es solche gibt, durch Konstruktion solcher Schaltkreise, oder durch Angabe kurzer Beweise der Clique-Tautologien im Lovász-Schrijver-System (im negativen Fall).
Ferner sollen weitere in der Praxis verwendete Einschränkungen der Resolution exponentiell vom uneingeschränkten Kalkül getrennt werden. So soll versucht werden, die superpolynomialen unteren Schranken für negative Resolution von Goerdt [11] zu verbessern. Dies wäre von besonderem Interesse für die Anwendung, da sich via Dualität die gleichen Schranken für positive Resolution ergäben, und letztere in der Praxis – als Hyperresolution – häufig verwendet wird.
Andere zu betrachtende Einschränkungen sind z.B. lineare Resolution, sowie solche, die nicht logisch vollständig, aber für die Anwendung wichtig sind, wie Hornklausel-Resolution und Einheitsklausel-Resolution.
Einen vielversprechenden Ansatz zum Beweis unterer Schranken bietet die Betrachtung der Weite von Resolutionsbeweisen, d.h. der maximalen Anzahl von Literalen in einer Klausel, die in der Arbeit von Ben-Sasson und Wigderson [3] eingeführt wurde. Obwohl die Beziehung zwischen Größe und Weite zur Angabe unterer Schranken für uneingeschränkte, dag-artige Beweise ausreicht, ist eine scharfe Charakterisierung der Beweisgröße durch die Weite nur für baumartige Resolution bekannt. Für andere Einschränkungen, wie die oben genannten, und insbesondere für den uneingeschränkten Kalkül ist also die genaue Beziehung dieser Komplexitätsmaße zu untersuchen.