Disjoint NP-pairs and propositional proof systems [Elektronische Ressource] / von Olaf Beyersdorff

Beyersdorff Olaf

Sujets

• Informatik
• Mathematics

Informations

• Publié par: humboldt-universitat_zu_berlin
• Publié le: 01 janvier 2006
• Nombre de lectures: 12
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

Disjoint NP-Pairs and Propositional Proof
Systems
DISSERTATION
zur Erlangung des akademischen Grades
doctor rerum naturalium
(Dr. rer. nat.)
im Fach Informatik
eingereicht an der
Mathematisch-Naturwissenschaftlichen Fakultät II
Humboldt-Universität zu Berlin
von
Herr Dipl.-Math. Olaf Beyersdorff
geboren am 18.08.1973 in Greifswald
Präsident der Humboldt-Universität zu Berlin:
Prof. Dr. Christoph Markschies
Dekan der Mathematisch-Naturwissenschaftlichen Fakultät II:
Prof. Dr. Wolfgang Coy
Gutachter:
1. Prof. Dr. Johannes Köbler
2. Prof. Dr. Martin Grohe
3. Prof. Dr. Pavel Pudlák
Tag der mündlichen Prüfung: 12. Juli 2006Abstract
Disjoint NP-pairs are an interesting complexity theoretic concept with
important applications in cryptography and propositional proof complexity.
In this dissertation we explore the connection between disjoint NP-pairs and
propositional proof complexity. This connection is fruitful for both fields.
Various disjoint NP-pairs have been associated with propositional proof sys-
tems which characterize important properties of these systems, yielding ap-
plications to areas such as automated theorem proving. Further, conditional
andunconditionallowerboundsfortheseparationofdisjointNP-pairscanbe
translated to results on lower bounds to the length of propositional proofs.
In this way disjoint NP-pairs have substantially contributed to the under-
standing of propositional proof systems.
Conversely,thisdissertationaimstotransferproof-theoreticknowledgeto
thetheoryofNP-pairs to gaina more detailedunderstanding of the structure
oftheclassofdisjointNP-pairsandinparticularoftheNP-pairsdefinedfrom
propositionalproofsystems. ForaproofsystemP weintroducethecomplex-
ity class DNPP(P) of all disjoint NP-pairs for which the disjointness of the
pair is efficiently provable in the proof systemP. We exhibit structural prop-
erties of proof systems which make the previously defined canonical NP-pairs
of these proof systems hard or complete for DNPP(P). Moreover we demon-
strate that non-equivalent proof systems can have equivalent canonical pairs
and that depending on the properties of the proof systems different scenarios
for DNPP(P) and the reductions between the canonical pairs exist. As an
important tool for our investigation we use the connection of propositional
proof systems and disjoint NP-pairs to theories of bounded arithmetic.
We also investigate a natural generalization of disjoint NP-pairs: instead
ofpairsweconsiderk-tuplesofpairwisedisjointNP-sets. Inourmainresultin
thispartweshowthatcompletedisjointNP-pairsexistifandonlyifcomplete
disjoint k-tuples of NP-sets exist for all k ≥ 2. Further, this is equivalent
to the existence of a propositional proof system in which the disjointness
of all tuples is shortly provable. We also show that a strengthening of this
conditions characterizes the existence of optimal proof systems.
Keywords:
disjoint NP-pairs, propositional proof systems, bounded arithmetic,
complexity theoryZusammenfassung
Die Theorie disjunkter NP-Paare, die auf natürliche Weise statt einzel-
ner Sprachen Paare von NP-Mengen zum Objekt ihres Studiums macht, ist
vor allem wegen ihrer Anwendungen in der Kryptografie und Beweistheorie
interessant. Im Zentrum dieser Dissertation steht die Analyse der Beziehung
zwischen disjunkten NP-Paaren und aussagenlogischen Beweissystemen. Ha-
ben die Anwendungen der NP-Paare in der Beweistheorie maßgeblich das
Verständnis aussagenlogischer Beweissysteme gefördert, so beschreiten wir
in dieser Arbeit gewissermaßen den umgekehrten Weg, indem wir Metho-
den der Beweistheorie zur genaueren Untersuchung des Verbands disjunkter
NP-Paare heranziehen.
InsbesondereordnenwirjedemBeweissystemP eineKlasseDNPP(P)von
NP-Paaren zu, deren Disjunktheit in dem Beweissystem P mit polynomiell
langenBeweisengezeigtwerdenkann.ZudiesenKlassenDNPP(P)zeigenwir
eine Reihe von Resultaten, die illustrieren, dass robust definierten Beweissy-
stemen sinnvolle Komplexitätsklassen DNPP(P) entsprechen. Als wichtiges
Hilfsmittel zur Untersuchung aussagenlogischer Beweissysteme und der dar-
aus abgeleiteten Klassen von NP-Paaren benutzen wir die Korrespondenz
starker Beweissysteme zu erststufigen arithmetischen Theorien, die gemein-
hin unter dem Schlagwort beschränkte Arithmetik zusammengefasst werden.
InderPraxistrifftmanstattaufzweihäufigaufeinegrößereZahlkonkur-
rierender Bedingungen. Daher widmen wir uns der Erweiterung der Theorie
disjunkter NP-Paare auf disjunkte Tupel von NP-Mengen. Unser Haupter-
gebnis in diesem Bereich besteht in der Charakterisierung der Fragen nach
der Existenz optimaler Beweissysteme und vollständiger NP-Paare mit Hilfe
disjunkter Tupel.
Schlagwörter:
disjunkte NP-Paare, aussagenlogische Beweissysteme, beschränkte
Arithmetik, KomplexitätstheorieContents
1 Introduction 1
1.1 Computational Complexity, Bounded Arithmetic, and Propo-
sitional Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
1.2 Disjoint NP-Pairs . . . . . . . . . . . . . . . . . . . . . . . . . 4
1.3 Organization of the Dissertation and Obtained Results . . . . 5
1.4 Published Parts . . . . . . . . . . . . . . . . . . . . . . . . . . 9
2 Propositional Proof Systems 10
2.1 Propositional Logic . . . . . . . . . . . . . . . . . . . . . . . . 10
2.2 Propl Proof Complexity . . . . . . . . . . . . . . . . . 12
2.3 Frege Systems and Their Extensions . . . . . . . . . . . . . . 15
2.4 Efficient Deduction . . . . . . . . . . . . . . . . . . . . . . . . 20
2.5 The Propositional Sequent Calculus . . . . . . . . . . . . . . . 22
2.6 Natural Properties of Proof Systems . . . . . . . . . . . . . . 24
3 Arithmetic Theories and Proof Systems 30
3.1 Theories of Bounded Arithmetic . . . . . . . . . . . . . . . . . 30
3.2 A Translation of Arithmetic Formulas into Propositional For-
mulas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
3.3 Coding Propositional Proofs in Bounded Arithmetic . . . . . . 36
3.4 Consistency Statements . . . . . . . . . . . . . . . . . . . . . 38
3.5 TheCorrespondenceBetweenArithmeticTheoriesandPropo-
sitional Proof Systems . . . . . . . . . . . . . . . . . . . . . . 39
3.6 The Correspondence for EF . . . . . . . . . . . . . . . . . . . 45
3.7 Regular Proof Systems . . . . . . . . . . . . . . . . . . . . . . 51
3.8 Comparing Properties of Proof Systems . . . . . . . . . . . . . 57
4 Disjoint NP-Pairs 60
4.1 Reductions Between NP-Pairs . . . . . . . . . . . . . . . . . . 60
4.2 The Simulation Order of Disjoint NP-Pairs . . . . . . . . . . . 64
4.3 Combinatorially Defined Pairs . . . . . . . . . . . . . . . . . . 68
iv4.4 NP-Pairs Characterize Properties of Proof Systems . . . . . . 70
4.4.1 The Canonical Pair of a Proof System . . . . . . . . . 70
4.4.2 The Canonical Pair and Automatizability . . . . . . . 71
4.4.3 The Interpolation Pair and Feasible Interpolation . . . 74
4.5 Representations of NP-Pairs . . . . . . . . . . . . . . . . . . . 77
4.6 The Complexity Class DNPP(P) . . . . . . . . . . . . . . . . 83
4.7 The Canonical Pair and the Reflection Principle . . . . . . . . 86
4.8 The Class DNPP(P) Under the Strong Reduction . . . . . . . 88
4.9 Canonical Complete Pairs . . . . . . . . . . . . . . . . . . . . 94
4.10 Symmetry of Disjoint NP-Pairs . . . . . . . . . . . . . . . . . 96
4.11 NP-Pairs and the Simulation Order of Proof Systems . . . . . 97
4.12 A Weak Reduction Between Proof Systems . . . . . . . . . . . 102
4.13 Proof Systems with Equivalent Canonical Pairs . . . . . . . . 105
4.14 Different Scenarios for DNPP(P) . . . . . . . . . . . . . . . . 110
4.15 On the Complexity of Ref(P) . . . . . . . . . . . . . . . . . . 111
4.16 Are Canonical Pairs Something Special? . . . . . . . . . . . . 114
5 Two Applications 119
5.1 Security of Public-Key Crypto Systems . . . . . . . . . . . . . 119
5.2 Pseudorandom Generators in Proof Complexity . . . . . . . . 121
6 Disjoint Tuples of NP-Sets 127
6.1 Basic Definitions and Properties . . . . . . . . . . . . . . . . . 127
6.2 Representable Disjoint Tuples of NP-Sets . . . . . . . . . . . . 130
6.3 Disjoint Tuples from Propositional Proof Systems . . . . . . . 132
6.4 Arithmetic Representations . . . . . . . . . . . . . . . . . . . 135
6.5 On Complete Disjoint Tuples of NP-Sets . . . . . . . . . . . . 138
Bibliography 145
vAcknowlegdements
First of all I am very grateful to my advisor Johannes
Köbler for his constant support and advice during the
preparation of this dissertation. He continously guided
my work with detailed suggestions and helpful com-
ments.
For encouraging support I am also very grateful to Jan
KrajíčekandPavelPudlákfromtheMathematicalInsti-
tute of the Academy of Sciences in Prague. Many help-
fulandstimulatingconversationsduringseveralvisitsto
Prague and during five Fall Schools at Pec pod Sněžkou
haveconsiderablydeepenedmyunderstandingofpropo-
sitional proof complexity. It was also Pavel Pudlák from
whom I first learned about the beautiful theory of dis-
joint NP-pairs at the Fall School 2001.
viChapter 1
Introduction
In den Werken des Menschen, wie in denen der
Natur, sind eigentlich die Absichten vorzü