Hi,
Ich sag jetzt mal nicht "es ist eigentlich ganz einfach", da ich nicht weiß ob ich das so einfach gefunden hätte,
wenn ich nicht den Hinweis gehabt hätte, dass es sich um eine Ungleichheit handeln soll.
Aber unabhängig davon ist die Klammerung ein gute Hilfe und die Art wie ein Rechner AND (*) und OR (+) Testet.
1) Bei X * Y müssen beide 1 sein, falls also X = 0 ist braucht man sich Y garnicht erst anschauen bzw. die Auswertung von Y findet nur statt, falls X=1
2) Bei X + Y braucht ja nur einer der Variablen 1 sein, falls also X = 1 ist braucht man sich Y garnicht erst anschauen.
Wenn man jetzt etwas um die Ecke denkt, wird Y erst ausgewertet wenn X = 0 ist
-b3 soll im weiteren not b3 bedeuten.
(a3 + -b3 ) * ((-a3 + -b3 ) * (a3 + b3 ) + (a2 + -b2 ) * ((-a2 + -b2 ) * (a2 + b2 ) + (a1 + -b1 )))
a) Sei also X=(a3 + -b3) und Y=Rest der Gleichung. Somit gilt X * Y
Falls man sich eine Werte Tabelle für a3 und b3 macht (nicht -b3), dann sieht man, dass nur für b3=1 und a3=0 X=0 ist, sonst X=1 (also für a3=b3 oder a3>b3), d.h nur in diesem Fall schau ich mir Y an.
b) nun sind wir in Y und das Können wir nun folgendermaßen aufteilen: X1=(-a3 + -b3 ) * (a3 + b3 ) und Y1=Rest der Gleichung. Somit gilt X1 + Y1.
X1 kann man mittels Boolesche Algebra oder mit WerteTabelle (oder man weiß es :( ) umformen in a3 XOR b3. Demzufolge wird hier nochmal explizit getestet ob a3!=b3 (ungleich) ist. Wie in 2) beschrieben interessieren wir uns für Y1 aber nur dann wenn X1 = 0 ist, d.h wenn a3=b3
c) nun können wir Y1 folgendermaßen aufteilen: X2=(a2 + -b2) und Y2=Rest. Somit wieder X2 * Y2
Diese Situation hatten wir schon in a) nur das wir es diesmal mit a2 und b2 zu tun haben. Ansonsten bleibt die Argumentation genau gleich.
d) Y2 können wir folgendermaßen aufteilen X3=(-a2 + -b2 ) * (a2 + b2 ) und Y3=(a1 + -b1 ). Somit gilt X3 + Y3
Hier kann man auch genau so argumentieren wie in b) nur das es sich diesmal um a2 und b2 handelt.
e) nun sind wir endlich bei (a1 + -b1) und das hier entscheidet ob größergleich oder echtgrößer. Falls man sich eine Wertetabelle mit a1 und b1 macht (nicht -b1) dann sieht man schnell, dass wir nur bei b1=1 und a1=0 eine 0 erzeugen. Oder man argumentiert wie bei 2) wir interessieren uns nur dann für b1 wenn a1 = 0 und dann ist doch Y3=0 wenn b1=1 und Y3=1 wenn b1=0... egal wie... raus kommt das Y3=1 wenn a1=b1 oder a1>b1 was für mich größergleich bedeutet. Deshalb sollte der ROBDD bei b1=0 auf 1 gehen und b1=1 auf a1
Gruß Tamas