Instituts-Logo Logik in der Informatik
Prof. Dr. Nicole Schweikardt 		Humboldt-Logo

Logbuch und Materialien zur Vorlesung Einführung in die Beweiskomplexität

Sommersemester 2017

Logbuch

Hier finden Sie (nach den Vorlesungen) Informationen zum Inhalt der einzelnen Vorlesungsstunden, Tipps zum Weiterlesen und gelegentlich ergänzende Bemerkungen.

Bitte beachten Sie: In der Vorlesung und der Übung werden viele wichtige Dinge (insbesondere Beweise, aber auch einiges andere) an der Tafel erklärt. Diese Dinge sind für die Veranstaltung "Einführung in die Beweiskomplexität" wesentlich und daher auch dann prüfungsrelevant, wenn sie nicht in den hier erhältlichen Materialien enthalten sind.

Di 18.04.2017

  • Einführung in das Thema "Beweiskomplexität" und Ausblick auf das Semester (Sem).
  • Definition eines aussagenlogischen Beweissystems nach Cook und Reckhow (CR79), p-beschränkte Beweisysteme, p-Simulation. Siehe Kapitel 1 in (Notizen).
  • In der nächsten Woche sind der Resolutionskalkül und der DPLL Algorithmus Thema. Bitte wiederholen Sie zur Vorbereitung Kapitel 2 (insbesondere 2.6 und 2.7) und Abschnitt 4.1 in (LogInf).
  • Die Auswertung der Umfrage finden Sie hier.

Mo 24.04.2017

  • Notationen und Definitionen zum Resolutionskalkül (Kapitel 2 in (Notizen))
  • Der DPLL-Algorithmus und baumartige Resolution (Kapitel 2.1 in (Notizen))
  • Ausgabe von Übungsblatt 1

Di 25.04.2017

  • Resolutionsspiel, das die Weite und Tiefe von Resolutionswiderlegungen charakterisiert (Kapitel 2.2 in (Notizen))
  • Das Black-Pebble Spiel, eine untere Schranke für Pyramiden (Kapitel 2.3 in (Notizen), siehe auch Theorem 4.8 in (N15)) und untere Schranken an die Tiefe von Black-Pebble-Formeln (Kapitel 2.3 in (Notizen))

Di 02.05.2017

  • Das Prover-Delayer-Spiel zum Beweisen unterer Schranken an die Größe von baumartigen Resolutionswiderlegungen (Kapitel 2.4 in (Notizen))
  • XOR-Substitution (Kapitel 2.5 in (Notizen)), Übung: Bestimmen Sie $\{x,\overline{y}\}[\oplus]$
  • Abschluss des Beweises von Satz 2.20 (eine exponentielle untere Schranke für baumartige Resolution: $D_T(F \vdash \emptyset)=2^{\Omega\bigl(\sqrt{\|F\|}\bigr)}$)

Mo 08.05.2017

  • Untere Schranke für baumartige Resolutionswiderlegungen des Taubenschlagprinzips via Prover-Delayer-Spielen (Übung)
  • Zusammenhang zwischen Länge und Weite baumartiger Widerlegungen (Kapitel 2.5 in (Notizen)) siehe auch (BW01).
  • Untere Schranke für baumartige Resolutionswiderlegungen des Taubenschlagprinzips via Resolutionsweite und Extensionsvariablen (siehe auch (BW01)).
  • Ausgabe von Übungsblatt 2

Di 09.05.2017

  • Zusammenhang zwischen Länge und Weite von Resolutionswiderlegungen (Satz 2.24 in (Notizen) = Theorem 3.5 in (BW01)).
  • Eine exponentielle untere Schranke für G-PHP (mit Expandergraphen G) via Resolutionsweite, Satz von Haken als Korollar (Kapitel 2.7 in (Notizen), siehe auch (BW01) Theorem 4.15).

Mo 15.05.2017

Di 16.05.2017

Mo 22.05.2017

  • Existenz von Boundary-Expandern (Kapitel 2.8 in (Notizen))
  • Zusammenfassung und Abschluss von Kapitel 2

Di 23.05.2017

  • Kapitel 3: Cutting Planes, Simulation von Resolution, Effizientes Widerlegen von $PHP^{n+1}_n$ wird Aufgabe im nächsten Übungsblatt sein
  • Die Interpolationsmethode, Definition Interpolante, Beweis von Satz 3.4, Seiten 3-1 bis 3-8 in (Notizen). Dieser Teil der Vorlesung orientiert sich an Pudlaks Originalarbeit (P97) (Abschnitt 1-4).

Mo 29.05.2017

  • Interpolationsmethode (Wiederholung Satz 3.4 und Beweis von Satz 3.5).
  • Clique-Formeln als ein erstes Beispiel für eine Formelmenge mit großen interpolierenden Schaltkreisen (ohne Beweis, siehe hierzu (P97) Abschnitt 5).
  • Kaputte-Fliegengitter-Formeln als ein weiteres Beispiel.

Di 30.05.2017

  • Eine untere Schranke an die Größe monotoner reeller Schaltkreise für kaputte Fliegengitter. Details zum Beweis finden Sie in (HC99).
  • Ausgabe von Übungsblatt 3

Mo 12.06.2017

Di 13.06.2017

  • Algebraische Beweissysteme (Kapitel 4, Seiten 1-10 in den (Notizen)):
  • Nullstellensatz (Definition, Korrektheit, Vollständigkeit)
  • Polynomkalkül (Simulation von Nullstellensatz und Resolution beschränkten Grades)
  • $\Omega(n/\log n)$ untere Schranke an den Grad von Nullstellensatzwiderlegungen

Mo 19.06.2017

  • Lehrevaluation
  • Wiederholung: untere Schranken für Nullstellensatz
  • ML-Polynomkalkül und ein $O(n^{3d})$ Algorithmus zum Finden von Ableitungen vom Grad $d$
  • Zum Nacharbeiten siehe auch Kapitel 5.5.2 in (CK02) und (CEI96)

Di 20.06.2017

  • Korrektheit des Algorithmus zum Bestimmen einer Basis der ableitbaren Polynome
  • Fourier-Repräsentation, Binomableitungen, Gauß-Kalkül (S. 4-18 bis 4-23 in den (Notizen))
  • Ausgabe von Übungsblatt 4

Mo 26.06.2017

  • Abgabe und Auswertung von Übungsblatt 4

Di 27.06.2017

  • Eine $\Omega(n)$ untere Schranke an die Weite im Gauß-Kalkül (Abschnitt 4.6 in den (Notizen))
  • Start mit Abschnitt 4.7, Lemma 4.21 zum Aufwärmen

Di 04.07.2017

  • Exponentielle untere Schranken für den Polynomkalkül und Abschluss von Kapitel 4
  • Start Kapitel 5: Definition Sum-of-Squares Kalkül.

Mo 10.07.2017

  • Finden von Grad-d SOS Widerlegungen mit Hilfe eines semidefiniten Programms der Größe $n^{O(d)}$. Zu aktuellen Entwicklungen bezüglich der Länge von SOS-Beweisen (dass die Kodierung der Koeffizienten der Polynome einer Grad-2 SOS-Widerlegung exponentielle Länge haben kann) siehe https://eccc.weizmann.ac.il/report/2016/141/ und https://arxiv.org/abs/1702.05139.
  • SOS vom Grad $2w$ simuliert Resolution der Weite $w$ (Satz 5.4).
  • Eine untere Schranke an den Grad von SOS Widerlegungen: Beweis von Satz 5.5 und Definition der Abbildung $\widetilde D$ in Lemma 5.6.

Di 11.07.2017

  • Abgabe und Auswertung von Übungsblatt 5
  • Auswertung der Lehrevaluation
  • Eine Auswahl an Prüfungsfragen finden Sie hier.

Mo 17.07.2017

  • Abschluss der unteren Schranke an den Grad von SOS-Widerlegungen.
  • Eine aktuelle untere Schranke an die Größe von Koeffizienten in SOS-Ableitungen: https://arxiv.org/abs/1702.05139 Abschnitt 5.1.

Di 18.07.2017

  • Abschluss Sum-of-Squares Kalkül
  • Überblick Frege und extended Frege

Materialien

An dieser Stelle finden Sie Materialien und Notizen zur Vorlesung zum Download.

(LogInf) Nicole Schweikardt. Skript zur Vorlesung "Logik in der Informatik"
(Sem) Semesterplan (Grafik)
(Notizen) Notizen zur Vorlesung.
  (Kapitel 1) Errata: In Definition 1.5 fehlt am Ende noch "… mit $(w,y)\in R$ und $\vert{}y\vert{} \leq \vert{}x\vert{}^c$."
  (Kapitel 2) S. 1 - 8
  (Kapitel 2) S. 9 - 11 (war Übungsaufgabe)
  (Kapitel 2) S. 12 - 30 Errata: In Lemma 2.18 muss es $w(F[\oplus]\vdash \emptyset)\leq 2\cdot w(F\vdash\emptyset) + 1$ heißen (und nicht $w(F[\oplus]\vdash \emptyset)\leq 2\cdot w(F\vdash\emptyset)$). Im Beweis von Satz 2.24 ist der Induktionsanfang $n=1$ und nicht $n=0$. Ergänzung: Beweis von Lemma 2.21 (S. 25a)
  (Kapitel 2) S. 31 - 38 Errata: Damit $2^{\Omega\bigl(\vert{}\vert{}G_n-PHP\vert{}\vert{}\bigr)}$ in Satz 2.29 brauchen wir Expandergraphen $G_n$ in denen auch der Grad auf der rechten Seiten beschränkt ist (und damit $\vert{}\vert{}G_n-PHP\vert{}\vert{}=O(n)$) - deren Existenz beweisen wir in Abschnitt 2.8.
  (Kapitel 2) S. 39 - 45
  (Kapitel 3) S. 1 - 11 Errata: In Satz 3.5 erhalten wir einen Schaltkreis mit s Gattern, allerdings haben die Gatter für die Axiome unbeschränkten fan-in. Diese können aber durch Additionsgatter mit fan-in 2 ersetzt werden, wodurch sich die Anzahl der Gatter im Schaltkreis auf $O(s+\vert{}\vert{}F\vert{}\vert{})$ erhöht.
  (Kapitel 3) S. 12 - 18
  (Kapitel 3) S. 19 - 21 Errata: In dem Bruch $\frac{A}{B}=\frac{(m^2-2)!}{2(km)^{r/2}(m^2-m)^{r/2}(m^2-2-r)!}$ im Beweis von Satz 3.7 fehlte noch der Faktor 2 im Nenner.
  (Kapitel 4) S. 1 - 10
  (Kapitel 4) S. 11 - 17
  (Kapitel 4) S. 18 - 23
  (Kapitel 4) S. 24 - 36
  (Kapitel 4) S. 37
  (Kapitel 5) S. 1 - 7
  (Kapitel 5) S. 8 - 16
  (Kapitel 5) S. 17 - 24, (Kapitel 6)

Literatur

Eine Liste mit Originalliteratur mit Bezug zur Vorlesung. Die Links verweisen entweder auf öffentlich zugängliche Quellen oder auf Verlagsseiten, die vom Universitätsnetz aus erreichbar sind. Bei Problemen mit der Bereitstellung wenden Sie sich bitte an den Dozenten.

(CR79) Cook, Reckhow. The relative efficiency of propositional proof systems. In: JOURNAL OF SYMBOLIC LOGIC, vol. 44, no. 1. LINK
(BIW04) Ben-Sasson, Impagliazzo, Wigderson. Near Optimal Separation Of Tree-Like And General Resolution. In: Combinatorica, September 2004, Volume 24, Issue 4, pp. 585–603. LINK
(N15) Jakob Nordström. New Wine into Old Wineskins: A Survey of Some Pebbling Classics with Supplemental Results. Manuskript. LINK
(BW01) Ben-Sasson, Wigderson. Short Proofs Are Narrow - Resolution Made Simple LINK
(H85) Haken. The intractability of resolution. In: Theoretical Computer Science, vol. 39. LINK
(M06) Melkebeek, Berg, Van Gael. Lecture 2: Existence of Expanders LINK (enthält ein ähnliches Argument, wie das in der Vorlesung, allerdings ist der Grad auf der rechten Seite des Expanders nicht beschränkt)
(P97) Pudlak. Lower Bounds for Resolution and Cutting Plane Proofs and Monotone Computations. In: Journal of Symbolic Logic, vol. 62, no. 3. LINK
(HC99) Haken, Cook. An Exponential Lower Bound for the Size of Monotone Real Circuits. In: Journal of Computer and System Sciences, vol. 58, no. 2. LINK
(CK02) Clote, Kranakis. Boolean Functions and Computation Models. Springer 2002.
(CEI96) Clegg, Edmonds, Impagliazzo. Using the Groebner basis algorithm to find proofs of unsatisfiability. In: Proc. STOC'96. S. 174-183 LINK
   

Author: Christoph Berkholz

Created: 2017-07-19 Mi 13:21

Emacs 24.5.1 (Org mode 8.2.10)

Validate