Verallgemeinerte Polynome. 

SUM_x(p) := p(x=0) + p(x=1)

Spaeter noch andere Operatoren. 

Wir uebersetzen eine Boole'sche Formel wie folgt in ein Polynom (ueber
denselben Variablen)

[x] = x
[phi | psi] = 1 - (1-[phi])(1-[psi])
[phi | psi | rho] = 1 - (1-[phi])(1-[psi])(1-[rho]) automatisch
[~phi] = 1-[phi]
[phi&psi] = [phi].[psi]

Es gilt: phi unerfuellbar: [phi]=0 fuer alle 0,1 Zuweisungen an die
Variablen. 

Ist phi in 3KNF, so ist der Grad von [phi]=3m, wobei m die Zahl der
Klauseln ist. 

Die Formel phi ist also unerfuellbar, genau dann wenn

SUM_x1(SUM_x2(...SUM_xk([phi])...) = 0 

Dies gilt es durch ein IP zu bestaetigen. Zunaechst beachten wir, dass
alle Zwischenergebnisse, die in der Auswertung des verallg Polynoms
auftreten moegen, durch 2^k beschraenkt sind. Rechnen wir also modulo
einer Primzahl p > 2^k, so treten keine Rechenfehler auf. Sei also
solch eine Primzahl fixiert. Genauer gesagt, kann der Prover diese
uebermitteln und es dem Verifier ueberlassen, einen Primzahltest
durchzufuehren. Man kann zeigen, dass eine solche Primzahl
polynomialer Laenge existiert. 

Hinfort werden also alle Berechungen mod p durchgefuehrt, ohne dies
jeweils explizit zu erwaehnen. 

Zu Beginn jeder Runde liegt ein verallgemeinertes Polynom in Variablen
y1..yi vor, sowie eine Belegung der Variablen a1..ai in Z/Zp und ein
vorgebliches Ergebnis b:Z/Zp. Der Prover hat die Aufgabe den Verifier
davon zu ueberzeugen, dass p(a1..ai)=b. 

Am Anfang ist natuerlich p = SUM...[phi], i=0 und b=0. Was ja
gleichbedeutend mit der Unerfuellbarkeit der Formel phi ist. 

Ist p = xi, so prueft der Verifier ab, ob b=ai. Keine Interaktion ist
hierfuer erforderlich. 

Ist p=p1.p2, so wird der Prover die beiden Teilergebnisse b1 und
b2 uebermitteln; der Verifier prueft, ob b1.b2 = b. In der naechsten
Runde wird dann p1(as)=b1 und p2(as)=b2 ueberprueft. 

Analog geht man vor, wenn p=p1+p2 oder p=p1-p2 ist. 

Man beachte, dass wenn p nicht den Operator SUM enthaelt keine echte
Interaktion stattfindet und die Verifikation einfach darauf
hinauslaeuft, dass der Verifier schaut, ob tatsaechlich p(as)=b
ist. Tritt dagegen der Operator SUM auf, so reichen die Ressourcen von
Verifier nicht aus, um diese Auswertung vorzunehmen; er benoetigt die
Hilfe des Verifiers. 

Hier muss der Prover die Koeffizienten (in Z/pZ) des Polynoms in x
p1(as,x) uebermitteln. Der Grad dieses Polynoms ist beschraenkt durch
den Grad des urpsruenglich gegebenen Polynoms mit dem das Protokoll
begonnen wurde. 

Seien also r_d ... r_0 diese Koeffizienten und r(x) =
r_d.x^d+...r_1.x+r_0 das entsprechende Polynom. Zunaechst prueft der
Verifier, ob r(0)+r(1)=b. Falls ja, so sollte der Prover bestaetigen,
dass das uebermittelte Polynom r(x) tatsaechlich uebereinstimmt mit
dem Rest p1(as,x). Damit dies wiederum in das beschriebene Format
kommt, waehlt der Verifier eine Zufallszahl in Z/pZ und fordert den
Prover auf, zu verifizieren, dass r(b) = p1(as,b) ist. 

Damit ist das Protokoll beschrieben. Es verbleibt die
Wahrscheinlichkeitsabschaetzung. 


Zunaechst ist festzustellen, dass wenn p(as) tatsaechlich gleich b
ist, so kann der Prover immer wunschgemaess antworten und V akzeptiert
mit Sicherheit. Es verbleibt die Abschaetzung der
Akzeptanzwahrscheinlichkeit (nach oben), falls p(as) =/= b. Hier
induzieren wir (ergebnisoffen) ueber die Anzahl der Runden. 

Ist diese gleich 0, so ist p eine Variable oder Konstante und die
Akzeptanz ist 0. 

Ist p=p1.p2, so muss entweder  p1(as)=/=b1 oder p2(as)=/=b2 sein. Dh
die  Akzeptanz ist gleich der bei der vorhergehenden Runde. 

Ist schliesslich p = SUM_x(p) so kann es passieren, dass wir zufaellig
eine Nullstelle des Polynoms (vom Grade 3m) erwischen. Die
Wahrscheinlichkeit dafuer ist aber nur 3m/p. Die Wahrscheinlichkeit,
dass n Runden in Ordnung gehen ist somit (1-3m/p)^n. Das aber ist
gross genug, wenn p = Omega(2^n). 


Fuer QBF statt nur co-3SAT verwendet man statt SUM die Operatoren 
 
EX_x(p)  = 1 - (1-p(x=0))(1-p(x=1))
ALL_x(p) = p(x=0)p(x=1)
RED_x(p) = p(x=0) + x.(p(x=1)-p(x=0))

Hier entsprechen EX, ALL der existentiellen bzw universellen
Quantifizierung ueber die Variable x und RED_x reduziert den Grad in x
auf 1 unter Beibehaltung des Wertverlaufs auf 0-1-Folgen. Durch
sukzessive Anwendung dieser Operatoren kann man somit einer QBF
Formel f der Laenge n einen
verallgemeinerten arithmetischen Ausdruck [f] zuordnen, derart dass
f=1, gdw f=TRUE. Letzteres kann dann durch ein IP Protokoll bestaetigt
werden.