Satz von Karp-Lipton: Wenn es polynomiell grosse Schaltkreise fuer SAT gibt, dann kollabiert die PH auf der 2. Stufe. Erlaeuterung: Die Voraussetzung des Satzes bedeutet, dass ein Polynom s(n) existiert und fuer jedes n ein boolescher Schaltkreis C_n der Groesse s(n) und mit n Eingaengen, sodass fuer alle aussagenlogischen Formeln phi mit |phi|<=n gilt C_n(phi)=1 <=> phi:SAT. Hierbei bedeutet C_n(phi) den Output des Schaltkreises C_n, wenn an seinen n Eingaengen die Binaerkodierung der Formel phi eingespeist wird. Der Schaltkreis C_n ist also ein "SAT-Chip", der das SAT-Problem fuer alle Instanzen der *festen* Groesse <=n loesen kann. Wichtig ist, dass C_n als Schaltkreis nur polynomielle Groesse hat. Solche Schaltkreise exponentieller Groesse lassen sich leicht angeben. Sie koennten z.B. die gesamte Wahrheitstafel der Groesse 2^n als grosse Fallunterscheidung festverdrahten. Liegt solch ein Schaltkreis C_n vor, so kann er leicht in einen Schaltkreis D_n von ebenfalls polynomieller Groesse umgebaut werden, der im Falle einer positiven Antwort auch noch eine erfuellende Belegung liefert. Hat etwa phi die Variablen x1..xm, so ergibt sich D_n aus folgendem Pseudocode: if (C_n(phi)) return (_,false); if (C_n(phi[x1:=true])) v1=true; else v1=false; if (C_n(phi[x1:=v1,x2:=true])) v2=true; else v2=false; if (C_n(phi[x1:=v1,x2:=v2,x3:=true])) v3=true; else v3=false; ... if (C_n(phi[x1:=v1,x2:=v2,...,x(m-1):=v(m-1),xm:=true])) vm=true; else vm=false; return ([x1->v1,\dots,xm->vm],true) Es ist klar, dass die Groesse von D_n ebenfalls polynomiell beschraenkt ist, sagen wir |D_n|<=q(n) und dass fuer |phi|<=n gilt: phi:SAT <==> D_n(phi)=(eta,true) & eta|=phi Wir nennen solch einen Schaltkreis "selbstzertifizierenden SAT-Tester". Die Tatsache, dass ein solcher aus C_n gewonnen werden kann, bezeichnet man als "Selbstreduzierbarkeit von SAT". Jetzt zum Beweis des Satzes. Wir zeigen zunaechst Pi_2^P <= Sigma_2^P. Wir fixieren L:Pi_2^P, also x:L <=> forall_p(|x|) y.exists_p(|x|) z. (x,y,z):L' wobei p ein Polynom ist und L':P. Erinnerung: exists_n x.A(x) bedeutet exists x.|x|<=n & A(x). Es ist nunmehr: x:L <=> exists_s(q(t(|x|))) D. "D ist selbstzertifizierender SAT Tester fuer Groesse n=t(|x|)" & forall_p(|x|) y.D("exists_p(|x|) z.(x,y,z):L'")=(_,true) Hier steht "exists_p(|x|) z.(x,y,z):L'" fuer eine Boolesche Formel, die erfuellbar ist, gdw exists_p(|x|) z.(x,y,z):L' und t(|x|) ist ihre Groesse. Klar kann t polynomiell gewaehlt werden. Die Variablen dieser Formel repraesentieren den Wert von z. Die Eigenschaft "D ist selbstzertifizierender SAT Tester fuer Groesse n=t(|x|)" kann nun wie folgt als Pi_1^P Formel geschrieben werden: "D ist selbstzertifizierender SAT Tester fuer Groesse n=t(|x|)" <=> forall_t(|x|) phi.D(phi)=(eta,true) & eta|=phi \/ D(phi)=(_,false) & forall_t(|x|) rho.rho|=/=phi <=> forall_t(|x|) phi.forall_t(|x|) rho. D(phi)=(eta,true) & eta|=phi \/ D(phi)=(_,false) & rho|=/=phi Somit gilt x:L <=> exists_s(q(t(|x|))) D. forall_t(|x|) phi.forall_t(|x|) rho. forall_p(|x|) y. (D(phi)=(eta,true) & eta|=phi \/ D(phi)=(_,false) & rho|=/=phi) & D("exists_p(|x|) z.(x,y,z):L'")=(_,true) was das geforderte Sigma_2^P Format hat. Der Kollaps der PH auf die zweite Stufe ergibt sich daraus als einfache praedikatenlogische Konsequenz.