Announcement

Collapse
No announcement yet.

Compurer Aided Verification - Übungsblatt 1

Collapse
X
  • Filter
  • Time
  • Show
Clear All
new 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
    Wie geht ihr vor bei Exercise2? Zuerst die Tautologien berechnen und dann BDD zeichnen?

    Comment


    • #3
      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).
      de.lernu.net, lingwadeplaneta.info

      Comment


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

        Comment


        • #5
          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).
          de.lernu.net, lingwadeplaneta.info

          Comment


          • #6
            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?

            Comment


            • #7
              Wie gehst du vor beim Bsp 3?

              Comment


              • #8
                Ü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
                de.lernu.net, lingwadeplaneta.info

                Comment


                • #9
                  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?

                  Comment

                  Working...
                  X