Compurer Aided Verification - Übungsblatt 1

[m4rS]

In den ersten Aufgaben sollen wir ja BDDs finden, und BDDs sind ja als DAGs beschrieben. Sind BDTs aber nicht eigentlich auch DAGs? Canonical Form ist ja nicht gefordert, oder?

Zu 1.) Jemand eine Ahnung, was da genau mit der Angabe gemeint ist? "The Boolean functions, that are always false and always true". Da könnte man ja irgendwelche Tautologien oder Kontradiktionen nehmen, oder ist da was spezielles gemeint?

[zero8]

Wie geht ihr vor bei Exercise2? Zuerst die Tautologien berechnen und dann BDD zeichnen?

[Dimitrij]

In den ersten Aufgaben sollen wir ja BDDs finden, und BDDs sind ja als DAGs beschrieben. Sind BDTs aber nicht eigentlich auch DAGs? Canonical Form ist ja nicht gefordert, oder?

Zu 1.) Jemand eine Ahnung, was da genau mit der Angabe gemeint ist? "The Boolean functions, that are always false and always true". Da könnte man ja irgendwelche Tautologien oder Kontradiktionen nehmen, oder ist da was spezielles gemeint?

Exercise 1:
Das sind einfach BDDs, die nur aus einem einzigen Knoten bestehen, nämlich aus dem Terminalvertex mit Wert 0 (für always false) bzw. Wert 1 (für always true).

[zero8]

Gibt es irgendwo Beispiele wie man BDDs für funktionen zeichnet? Wie soll man bei Funktionen vorgehen?

[Dimitrij]

Wie geht ihr vor bei Exercise2? Zuerst die Tautologien berechnen und dann BDD zeichnen?

Was für Tautologien?
Man beginnt einfach mit einer beliebigen Variablen und schaut, welche Formel man erhält, wenn man diese Variable auf 0 bzw. 1 setzt. Wenn man z.B. a auf 0 setzt, erhält man b->(c und b). Dann macht man genauso weiter. Wenn man in b->(c und b) die Variable b auf 0 setzt, erhält man 0->0, also 1.
Bei diesem Beispiel ist es am besten, mit b zu beginnen (führt zu kleinerem BDD).

[zero8]

ich habe die Tabelle für a,b,c a v b, a & b, (a v b) -> (c & b) erstellt und die Werter für (a v b) -> (c & b) berechnet. Dannhabe ich mit a < b < c BDD berechnet.
Machst du es anders?

[zero8]

Wie gehst du vor beim Bsp 3?

[Dimitrij]

Über BDDs steht auch etwas auf den alten Folien aus Formale Methoden der Informatik: http://www.logic.at/lvas/185291/10S/
und im Buch, das dort angeführt wird (gibt es in der Bibliothek).

Für Exercise 5 hab ich mir das angeschaut: http://www.cs.cmu.edu/~bryant/pubdir/ieeetc86.pdf

[zero8]

Danke für Info. Ich habe es bisschen angeschaut. Ich sehe das so:
X = x1x2x3x4
Y = y1y2y3y4

X + 1 = Y

Smoit habe ich:
0000 + 1 = 0001
0001 + 1 = 0010
.
.
.
Wenn man das so darstellt (so wie in der VO):
X
0/ \1
FI PSI
bekommen wie: (X & PSI) oder (-X & FI)
Geht das so, oder bin ich ganz falsch?