Results 1 to 9 of 9

Thread: Compurer Aided Verification - Übungsblatt 1

  1. #1
    Dipl.Ing
    Join Date
    Apr 2008
    Posts
    1,519
    Thanks
    64
    Thanked 100 Times in 85 Posts

    Compurer Aided Verification - Übungsblatt 1

    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?
    Random nontrivial stuff: http://rjlipton.wordpress.com/ Proofs for: P=NP, P!=NP, P vs NP is undecidable: http://www.win.tue.nl/~gwoegi/P-versus-NP.htm

  2. #2
    Elite
    Join Date
    Oct 2004
    Posts
    346
    Thanks
    3
    Thanked 2 Times in 2 Posts
    Wie geht ihr vor bei Exercise2? Zuerst die Tautologien berechnen und dann BDD zeichnen?

  3. #3
    Baccalaureus
    Join Date
    Feb 2002
    Location
    Wien
    Posts
    530
    Thanks
    3
    Thanked 117 Times in 72 Posts
    Quote Originally Posted by m4rS View Post
    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).

  4. #4
    Elite
    Join Date
    Oct 2004
    Posts
    346
    Thanks
    3
    Thanked 2 Times in 2 Posts
    Gibt es irgendwo Beispiele wie man BDDs für funktionen zeichnet? Wie soll man bei Funktionen vorgehen?

  5. #5
    Baccalaureus
    Join Date
    Feb 2002
    Location
    Wien
    Posts
    530
    Thanks
    3
    Thanked 117 Times in 72 Posts
    Quote Originally Posted by zero8 View Post
    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).

  6. #6
    Elite
    Join Date
    Oct 2004
    Posts
    346
    Thanks
    3
    Thanked 2 Times in 2 Posts
    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?

  7. #7
    Elite
    Join Date
    Oct 2004
    Posts
    346
    Thanks
    3
    Thanked 2 Times in 2 Posts
    Wie gehst du vor beim Bsp 3?

  8. #8
    Baccalaureus
    Join Date
    Feb 2002
    Location
    Wien
    Posts
    530
    Thanks
    3
    Thanked 117 Times in 72 Posts
    Ü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

  9. #9
    Elite
    Join Date
    Oct 2004
    Posts
    346
    Thanks
    3
    Thanked 2 Times in 2 Posts
    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?

Bookmarks

Posting Permissions

  • You may not post new threads
  • You may not post replies
  • You may not post attachments
  • You may not edit your posts
  •