Forschungsprojekt

Komplexität aussagenlogischer Beweissysteme und monotoner Schaltkreise, sowie deren Zusammenhang mittels monotoner effektiver Interpolation.

Jan Johannsen


Zusammenfassung

Es sollen Probleme aus der Komplexitätstheorie monotoner Schaltkreise und ihre Anwendung auf Probleme aus der Theorie der Komplexität aussagenlogischer Beweissysteme untersucht werden. Insbesondere sollen untere Schranken an die Tiefe und Größe boolescher Schaltkreise verbessert und auf weitere Klassen monotoner Schaltkreise (boolesche Schaltkreise mit unbeschränktem Eingangsgrad, monotone reelle Schaltkreise) verallgemeinert werden. Als Anwendung folgen neue und verbesserte untere Schranken für aussagenlogische Beweissysteme, etwa Varianten des Cutting-Planes Systems, mittels der Methode der effektiven monotonen Interpolation. Weiterhin soll untersucht werden, inwieweit diese Interpolationsmethode auf verschiedene, in der Literatur vorgeschlagene und neue, Erweiterungen von Cutting-Planes-Beweissystemen verallgemeinert werden kann.

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.


Stand der Forschung

Eines der Hauptprobleme der Komplexitätstheorie ist es, superpolynomiale untere Schranken an die Größe von booleschen Schaltkreisen, die ein konkretes Problem in NP berechnen, zu zeigen. Obwohl ein einfaches Abzählargument zeigt, daß fast alle booleschen Funktionen Schaltkreise exponentieller Größe erfordern, sind bislang für konkrete Probleme nicht einmal superlineare untere Schranken bekannt. Aus diesem Grund werden zur Entwicklung von Anschauung und Beweistechniken eingeschränkte Klassen von Schaltkreisen betrachtet. Eine der erfolgreichsten Forschungsrichtungen in diesem Sinne betrachtet die Komplexität monotoner boolescher Schaltkreise, d.h. solcher, die nur aus UND- und ODER-Gattern, aber ohne Negationen, aufgebaut sind.

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.


Eigene Vorarbeiten

In meiner Arbeit [a] habe ich die von Karchmer und Wigderson [17] gegebenen unteren Schranken an die Tiefe monotoner Schaltkreise und die Größe monotoner Formeln auf den Fall monotoner reeller Schaltkreise verallgemeinert. Daraus folgt, daß dag-artige Cutting-Planes Beweise superpolynomial kürzer sein können als baumartige. Diese Trennung konnten wir in der Arbeit [b] zu einer schwach exponentiellen verbessern, indem wir die unteren Schranken von Raz und McKenzie [24] für monotone reelle Schaltkreise verallgemeinert und geeignete Tautologien, deren Interpolanten das Gen-Problem lösen, konstruiert haben. Beide unteren Schranken wurden durch Angabe unterer Schranken an die (von Krajícek [19] eingeführte) reelle Kommunikationskomplexität des Karchmer-Wigderson-Spiels gezeigt.

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.


Relevante Veröffentlichungen

[a]
Johannsen, J.,"Lower Bounds for Monotone Real Circuit Depth and Formula Size and Tree-like Cutting Planes", Information Processing Letters 67 (1998), pp. 67-71.
[b]
Bonet, M.L., Esteban, J.L., Galesi, N. und Johannsen, J., "Exponential Separations between Restricted Resolution and Cutting Planes Proof Systems", eingereicht bei SIAM Journal on Computing, vorläufige Version in Proceedings of the 39th IEEE Symposium on Foundations of Computer Science (1998), pp. 638-647.
[c]
Johannsen, J., "Weak Bounded Arithmetic, the Diffie-Hellman Problem and Constable's Class K", Proceedings 14th IEEE Symposium on Logic in Computer Science, Trento 1999, pp. 268-274.

Ziele und Arbeitsprogramm

Bessere untere Schranken

Die in [b] gezeigte schwach exponentielle Trennung von baumartigen und dag-artigen Resolutionsbeweisen wurde von Ben-Sasson und Wigderson [3] zu einer echt exponentiellen, mit einer unteren Schranke der Form 2n/log n, verbessert. Wir wollen eine ähnlich starke Trennung von baumartigen gegenüber dag-artigen Cutting-Planes Beweisen erreichen.

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.

Monotone reelle vs. boolesche Schaltkreise

Ein wichtiges offenes Problem ist, ob die Verwendung großer Koeffizienten eine superpolynomiale Verkürzung von Cutting-Planes-Beweisen erlaubt, insbesondere, ob das System CP*, in dem die Koeffizienten polynomial beschränkt sind, echt schwächer ist als das volle System CP.

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.

Schaltkreise unbeschränkten Eingangsgrades

Im Folgenden verwende ich die von Grigni und Sipser [14] eingeführte Notation: für eine Schaltkreiskomplexitätsklasse C bezeichne mC die entsprechende Klasse von monotonen Schaltkreisen, bzw. die dadurch definierte Komplexitätsklasse. Das Resultat von Karchmer und Wigderson liest sich in dieser Notation als mNC1 < mNC2, und die Verallgemeinerung von Grigni und Sipser als mSAC1 co-mSAC1. Hierbei steht mNCi für die Klasse monotoner Schaltkreise der Tiefe O(logi n) und polynomialer Größe, mACi für die durch die entsprechenden Schaltkreise mit Gattern unbeschränkten Eingangsgrades definierte Klasse. Weiter ist mSACi durch Schaltkreise definiert, in denen die ODER-Gatter unbeschränkten, die UND-Gatter jedoch nur beschränkten Eingangsgrad haben, und co-mSACibezeichnet die duale Klasse, in denen nur die UND-Gatter unbeschränkten Eingangsgrad haben. Aus der Arbeit von Raz und McKenzie [24] folgt, daß für jedes i gilt mNCi < mNCi+1. Wir wollen diese Tiefenhierarchie auf monotone Schaltkreise mit unbeschränktem und semi-unbeschränktem Eingangsgrad verallgemeinern, mit dem Ziel, zu zeigen, daß im untenstehenden Inklusionsdiagramm für jedes i alle Inklusionen echt sind.

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.

Relationen zwischen Komplexitätsmaßen

Für monotone ebenso wie allgemeine, nicht-monotone boolesche Schaltkreise sind Schaltkreistiefe und Formelgröße im wesentlichen dasselbe Komplexitätsmaß, da sie mittels des Brent-Spira Theorems exponentiell verkoppelt sind. Für monotone reelle Schaltkreise sollte eine ähnliche Beziehung gelten. Offensichtlich ist der Logarithmus der Formelgröße eine untere Schranke für die Schaltkreistiefe, aber die umgekehrte Ungleichung ist in diesem Fall nicht bekannt.

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].

Erweiterungen von CP

Es soll untersucht werden, ob monotone effektive Interpolation durch monotone reelle Schaltkreise für das volle System R(CP) aus [20], also mit mehr als einer Ungleichung pro Klausel gilt. Für baumartige Beweise ist dies vermutlich der Fall. Es ist jedoch nicht auszuschließen, daß kurze dag-artige Beweise mit einer großen Zahl von Ungleichungen pro Klausel für die Clique-Tautologien existieren, oder daß diese Beweise überaupt keine effektive Interpolation erfüllen.

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).

Eingeschränkte Resolutionskalküle

Im Anschluß an die Ergebnisse der Arbeit [b] sollen weitere Fragen über die relative Komplexität von eingeschränkten Formen des Resolutionskalküls untersucht werden. Insbesondere wurde dort eine exponentielle Trennung der Davis-Putnam-Resolution von uneingeschränkter Resolution angegeben. In der Komplexität zwischen diesen liegt die reguläre Resolution, und es bleibt zu klären, zwischen welchen dieser Einschränkungen exponentielle Beweisverkürzungen möglich sind. Die naheliegende Vermutung ist, daß in beiden Fällen eine exponentielle Trennung vorliegt.

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.


Literatur

[1]
Alon, N. und Boppana, R., "The Monotone Circuit Complexity of Boolean Functions", Combinatorica 7 (1987), pp. 1-22.

[2]
Beigel, R., "When do Extra Majority Gates Help? Polylog(N) Majority Gates are Equivalent to One", Computational Complexity 4 (1994), pp. 314-324.

[3]
Ben-Sasson, E. und Wigderson, A., "Short Proofs Are Narrow - Resolution Made Simple", erscheint in Proceedings of the 31st ACM Symposium on Theory of Computing, 1999.

[4]
Bonet, M.L., Domingo, C., Gavalda, R., Pitassi, T. und Maciel, A. "Non-Automatizability of Bounded-Depth Frege Proofs", erscheint in Proceedings of the 14th IEEE Conference on Computational Complexity, 1999.

[5]
Bonet, M.L., Pitassi, T. und Raz, R., "Lower Bounds for Cutting Planes Proofs with Small Coefficients", Journal of Symbolic Logic 62 (1997), pp. 708-728.

[6]
Bonet, M.L., Pitassi, T. und Raz, R., "No Feasible Interpolaion for TC0-Frege Proofs", Proceedings of the 38th IEEE Symposium on Foundations of Computer Science (1997), pp. 254-263.

[7]
Cook, S. und Haken, A., "An Exponential Lower Bound for the Size of Monotone Real Circuits", Journal of Computer and System Sciences 58 (1999), pp. 326-335.

[8]
Cook, W., Coullard, C. und Turán, G., "On the Complexity of Cutting Plane Proofs", Discrete Applied Mathematics 18 (1987), pp. 25-38.

[9]
Fu, X., "Lower Bounds on Sizes of Cutting Planes Proofs for Modular Coloring Principles", in Beame, P. und Buss, S., Hrsg., Proof Complexity and Feasible Arithmetics, AMS 1998, pp. 135-148.

[10]
Goerdt, A., "Davis-Putnam Resolution versus Unrestricted Resolution", Annals of Mathematics and Artificial Intelligence 6 (1992), pp. 169-184.

[11]
Goerdt, A., "Unrestricted Resolution versus N-Resolution", Theoretical Computer Science 93 (1992), pp. 297-308.

[12]
Goerdt, A., "Regular Resolution versus Unrestricted Resolution", SIAM Journal on Computing 22 (1993), pp. 661-683.

[13]
Goldmann, M. und Håstad, J., "Monotone Circuits for Connectivity have Depth (log n)2-o(1)", SIAM Journal on Computing 27 (1998), pp. 1283-1294.

[14]
Grigni, M. und Sipser, M., "Monotone Complexity", in Paterson, M.S., Hrsg., Boolean Function Complexity, Cambridge University Press, 1992, pp. 57-75.

[15]
Haken, A. "The Intractability of Resolution", Theoretical Computer Science 39 (1985), pp. 297-308.

[16]
Jukna, S., "Combinatorics of Monotone Computations", erscheint in Combinatorica, vorläufige Version erhältlich als ECCC TR98-041, 1998.

[17]
Karchmer, M. und Wigderson, A., "Monotone Cicuits for Connectivity Require Superlogarithmic Depth", SIAM Journal on Discrete Mathematics 3 (1990), pp. 255-265.

[18]
Krajícek, J., "Interpolation Theorems, Lower Bounds for Proof Systems, and Independence Results for Bounded Arithmetic", Journal of Symbolic Logic 62 (1997), pp. 457-486.

[19]
Krajícek, J., "Interpolation by a Game", Mathematical Logic Quarterly 44 (1998), pp. 450-458.

[20]
Krajícek, J., "Discretely Ordered Modules as a First-Order Extension of the Cutting Planes Proof System", Journal of Symbolic Logic 63 (1998), pp. 1582-1596.

[21]
Krajícek, J. und Pudlák, P., "Some Consequences of Cryptographical Conjectures for S12 and EF", Information and Computation 140 (1998), pp. 82-94.

[22]
Pudlák, P., "Lower Bounds for Resolution and Cutting Planes Proofs and Monotone Computations", Journal of Symbolic Logic 6 (1997), pp. 981-998.

[23]
Pudlák, P., "On the Complexity of the Propositional Calculus", erscheint in Proceedings of Logic Colloquium 97, Springer Lecture Notes in Logic, 1999.

[24]
Raz, R. und McKenzie, P. "Separation of the Monotone NC Hierarchy", Proceedings of the 38th IEEE Symposium on Foundations of Computer Science (1997), pp. 234-243.

[25]
Raz, R. und Wigderson, A., "Monotone Circuits for Matching Require Linear Depth", Journal of the ACM 39 (1992), pp. 736-744.

[26]
Razborov, A. A., "Lower Bounds on the Monotone Complexity of Some Boolean Functions", Soviet Mathem. Doklady 31 (1985), pp. 354-357.

[27]
Razborov, A. A., "Unprovability of Lower Bounds on Circuit Size in Certain Fragments of Bounded Arithmetic", Izvestiya: Mathematics 59 (1995), pp. 205-227.

[28]
Rosenbloom, A., "Monotone Real Circuits Are More Powerful than Monotone Boolean Circuits", Information Processing Letters 61 (1997), pp. 161-164.

[29]
Tardos, É., "The Gap between Monotone and Nonmonotone Circuit Complexity is Exponential", Combinatorica 8 (1988), pp. 141-142.

[30]
Urquhart, A., "The Complexity of Propositional Proofs", Bulletin of Symbolic Logic 1 (1995), pp. 425-467.