Efﬁziente Implementierung von Binären Entscheidungsdiagrammen · – Kombinationen zum gleichen...

runekrauss.com

Effiziente Implementierung von Binären Entscheidungsdiagrammen

Einleitung

•  Repräsentation und Manipulation Boolescher Funktionen ist wichtig für viele Applikationen:–  Symbolische Simulation, Model Checking

•  Erstrebenswert, Variablen erstellen zu können und Operationen auf Funktionen zu erlauben

•  Funktionen können dargestellt werden durch Formeln und Schaltkreise (SKs)–  Benötigen viel Speicher–  Viele Funktionen haben eine exponentielle Größe–  Praktische Funktionen sollten effizient darstellbar sein

16.08.18 Implementierung von ROBDDs 2

Einleitung (2)•  Für Kompaktheit sowie Effizienz gibt es Binäre

Entscheidungsdiagramme (BDDs)–  Heuristische Methode zur Darstellung von Zuständen–  Datenstruktur für Logiksynthese und Verifikation

•  Welche Anforderungen an Boolesche Funktionen gibt es?–  Probleme: Äquivalenztest, SAT, ...–  Für Formeln und SKs im Allgemeinen NP-vollständig–  Reduzierte geordnete BDDs (ROBDDs) erlauben

häufig eine konstante Laufzeit!•  Aktuelle Pakete haben Schwachstellen!16.08.18 Implementierung von ROBDDs 3

Agenda

1.  Grundlagen2.  Entscheidungs- und Berechnungsprobleme3.  Bestandteile der Implementierung4.  Beispiel einer Ausführung5.  Experimentelle Ergebnisse


Grundlagen

•  Azyklischer Graph•  Innerer Knoten

–  Variablen–  low-Kind und high-

Kind als Nachfolger•  Blätter

–  Konstanten•  Zerlegungstyp ist die

Shannon-Dekomposition

16.08.18 Entscheidungsdiagramme 5

ROBDDs

•  Informationen kompakt Reduziert, wenn:–  es gibt keinen

nichtterminalen Knoten v mit Index x und (fv)x = (fv)x‘

–  es gibt keine verschiedenen Knoten v, w, die gleich markiert sind und deren low- und high-Kind (falls existent) jeweils identisch sind

16.08.18 Entscheidungsdiagramme 6

Satz von Bryant: Geordnete reduzierte BDDs sind kanonische Darstellungen Boolescher Funktionen.

Redundanz-Regel:

Isomorphie-Regel:

Äquivalenztest

Eingabe OBDDs Ga und Gb, wobei a, b ∈ Bn

Ausgabe JA, falls a = b, NEIN sonst Verfahren Ga und Gb zu Ga‘ und Gb‘ reduzieren, dann beide auf

Isomorphie testen. Komplexität O(|Ga| + |Gb|), da die Reduktion und der Isomorphie-Test

linear beschränkt sind.


Wenn a und b gemeinsam in einem ROBDD dargestellt werden, so genügt ein Test, ob die Zeiger für a und b auf denselben Knoten zeigen. ⇒ O(1)

Für Wahrheitstafeln ist die Laufzeit proportional zu 2n, für andere Darstellungen sind auch keine effizienten Verfahren bekannt.

Auswertungsproblem

Eingabe OBDD G für f ∈ Bn, eine Bel. x ∈ {0, 1}n

Ausgabe JA, falls f(x) = 1, NEIN sonst Verfahren Durchlaufe G von der Wurzel bis zu einem Blatt gemäß x.

Gebe anschließend dessen Markierung aus. Komplexität O(n), da jede Variable höchstens einmal getestet werden

darf.


Keine Verbesserung durch ein ROBDD möglich!

Für die anderen Darstellungen gilt ebenfalls ein linearer Aufwand, da die Anzahl der Aufrufe zur Auswertung durch die Größe der Formel beschränkt ist.

Was bietet das ROBDD-Paket?

•  Repräsentation von Booleschen Funktionen•  Synthese von BDD-Knoten

–  Einsatz von Hashtabellen–  Verwendung von Standard-Tripeln–  Speicherbereinigung–  Nutzung von komplementären Kanten

•  Umwandlung von Schaltkreisen in ROBDDs•  Lösen von Entscheidungs- und

Berechnungsproblemen


Implementierung•  Das Hauptproblem ist der Speicherplatz

–  Zwischenergebnisse können sehr groß werden–  Kleinere Optimierungen bereits sehr wichtig

•  Beispiel: Funktion via Beschreibung eines SKs–  Für jeden Baustein erfolgt eine Synthese–  Angabe oberer Schranken für einzelne Synthese-

Operationen (OPs) nicht möglich•  Anwendung vieler Tricks (bspw. not)

–  Vertauschen der Blätter 0, 1 (explizit in linearer Zeit)–  Geschickter in O(1) durch Festlegung einer

Interpretation der Blätter-Markierungen realisierbar16.08.18 Implementierung von ROBDDs 10

Implementierung: Bestandteile

Knoten Repräsentation der OBDDs, size_t für Indizes Manager Hält Operationen zur Manipulation von BDDs wie

die Erstellung von Variablen oder Synthese bereit, weiterhin werden hierüber Knoten visualisiert.

Unique-Table Diese Hashtabelle gewährleistet die Kanonizität und ermöglicht einen schnellen Zugriff auf Knoten.

Computed-Table Dieser Cache speichert bereits durchgeführte Operationen, sodass doppelte Berechnungen verhindert werden.

Speicherbereinigung Knoten besitzen einen Referenzzähler mit den Verweisen auf sich selbst, d. h. sollte die Referenz 0 betragen, so kann ein Knoten bereinigt werden.


•  Generisch (K für Schlüssel, E für Knoten bei den Tabellen) •  Basiert auf Indizes •  Einige Implementierungstricks wie z. B. bei not !

SBDDs•  Mehrere Funktionen

durch einen BDD darstellbar

•  Äquivalenztest einfach•  Mehrere Startknoten:

–  fA = x1(x2+x3) –  fB = x1‘(x2+x3) –  fC = x2+x3

•  Speicherplatz/Ber. können gespart werden


Knoten: BDDNode und DDNode•  Anwendung arbeitet mit Millionen von Knoten

–  Sollten daher so kompakt wie möglich sein•  Wichtigste Eigenschaft ist die Eindeutigkeit

–  Knoten v mit l(v) hat Kinder g, h (Markierung/Verweise)–  Über Index bzgl. Referenzen zu andere v‘s (2 Bytes)–  Knoten v wird mit ite(v, g, h) eindeutig identifiziert

•  Verweis auf einen Nachfolger der Kollisionskette–  Realisierung in einem gemeinsamen Vektor in der UT

(liegen eng beieinander, Pointer-Arithmetik (konstant)•  Referenzzähler für die Speicherbereinigung•  Ca. 22 Bytes bei max. 216 Variablen16.08.18 Implementierung von ROBDDs 13

ITE-Operator•  In einem BDD werden Boolesche OPs realisiert•  BDDs werden i. d. R. durch die Kombination von

mehreren BDDs erzeugt (Synthese)•  Kern des Paketes, der drei Operanden zur Ber.

von ite(f, g, h) = fg + f‘h (Shannon-Zerlegung, wenn f Entscheidungsvariable) benötigt–  Beispiel (Konjunktion): ite(f, g, 0) = f ⋅ g + f‘ ⋅ 0 = f ⋅ g

•  Alle ein- und zweistelligen Booleschen Operatoren können direkt darauf zurückgeführt werden.

•  Knoten speichert ein Tripel (Variable, Kinder)16.08.18 Implementierung von ROBDDs 14

ITE-Operator: Algorithmusprogram ite() ! input: f, g, h (OBDDs) ! output: ROBDD ite(f, g, h) ! res := BDDNode! node := DDNode! complementEdge := false! standardize(f, g, h, complementEdge) ! // Wenn z. B. f = 1 => g ! if (terminal) then! if (complementEdge = true) then! res := !res! return res; ! key := getKey( getDDNode(f), ..., getDDNode(h) ) ! if ( cT.hasNext(key, res) ) ! ... ! return res; ! top := index(f) ! f0 := getCofactor(f, top, low) ! f1 := getCofactor(f, top, high) ! ... ! t = ite(f1, g1, h1); ! e = ite(f0, g0, h0); ! if (t = e) then! return t; ! node := findAdd( top, getDDNode(t), getDDNode(e) ) ! cTable.insert(key, node) ! !

1.  Aufruf standardisieren2.  Terminalfall?3.  Wenn die Kante komplementär ist, so

muss das Ergebnis negiert werden4.  Generiere den Schlüssel5.  Gibt es den Knoten mit den Parametern

in der CT?6.  Ermittle die Kofaktoren von f !7.  Kreiere damit 2 Teilprobleme t, e

(wähle die Wurzelmarkierung xi aus, die in der Ordnung zuerst steht, wobei der höhere Index zuerst betrachtet wird)

8.  Überprüfung auf Isomorphie9.  Knoten nur in UT erstellen und Verweis

zurückgeben, wenn er noch nicht existiert

10.  Berechnung in CT speichern


Unique-Table (UT)

•  Wird als Hashtabelle (Index aus Suchwert) realisiert–  Kanonizität: g, h kan. ⇒ ∃ f ∈ R, falls ∃ (v,g,h) dafür–  Knoten werden gespeichert/wiederverwendet

•  Hashverfahren kann auch ineffizient sein–  Kollisionen nicht vermeidbar (n. injektiv) ⇒ Vermindern–  Kollision ⇒ Direkte Eintragung in Vektor als Nachfolger–  Die Performance von OPs hängt vom Bel.-Faktor

a = n/m ab–  Modulo- oder Multiplikationsverfahren


Computed-Table•  Cache, um Performance der Synthese zu steigern

–  Berechnete Ergebnisse abspeichern–  Isomorphe Teilgraphen nicht öfter betrachten–  Hashfunktion/Schlüssel optimal wählen–  Keine Kollisionsstrategie/Einträge überschreiben–  Einträge nicht bis zur Löschung speichern–  Keine Kanonizität und kein Suchvorgang nötig

•  Komplexität:–  Schlüssel → Alle Knoten–  Dynamisch (500.000) → Speicherplatz sparen


Komplementäre Kanten (CEs)•  Knoten f‘ wird nicht gespeichert, sondern eine

Kante auf f, die das complement-Bit (cB) setzt•  Bei Traversierung zählen, ob eine gerade oder

ungerade Anzahl von Kanten mit Label vorliegt–  Bei ungerader Anzahl wird d. Wert d. Senke negiert–  Nicht mehr bis auf Isomorphie eindeutig:

1.  Es gibt nur noch eine 1-Senke (geht auch umgekehrt)2.  Output-Inverter nur auf low-Kanten (high) erlaubt3.  Output-Inverter dürfen bei der Wurzel sein


CEs (2)


Sämtliche Regeln werden beim Aufruf von lookup bzw. put beachtet:

Das 0-Blatt wird entfernt und die Kanten normiert. Praktisch gesehen wird direkt bei der Synthese darauf geachtet (Überführung nicht notwendig). Bei ungerader Anzahl der Inverter den Ausgangswert negieren. Es wird also auch die Negation direkt im ROBDD gespeichert ⇒ O(1) Die Größenersparnis entspricht im best-Case dem Faktor 2 (Ø 7%). Wenn zwei der Argumente im Aufruf von ITE komplementär sind, so ist der Algorithmus quadratisch beschränkt. Zudem ist kein zusätzlicher Speicher notwendig, wenn der LSB von Zeigern zur Kodierung des cB benutzt wird (alle gängigen Rechner nutzen gerade Adressen, d. h. es ist 0).

Standard-Tripel (ST) für ITE

•  Mehrdeutige ITE-Aufrufe standardisieren–  Es gibt Parameter f1, f2, f3 und g1, g2, g3, sodass ite(f1, f2,

f3) = ite(g1, g2, g3), ∃i : fi ≠ gi ⇒ Äquivalenzrelation –  Kombinationen zum gleichen Ergebnis in ÄKs

zusammenfassen und Repräsentanten bestimmen–  CT wird klein gehalten/redundante Ber. vermeiden

•  Bestimmung des Standard-Tripels:1.  Erst Parameter umformen:

•  Z. B. ite(f, g, f‘) ⇒ ite(f, g, 1) (Negation des Anderen über CE)2.  Repräsentanten (Paar) aus der ÄK wählen:

•  Z. B. ite(f, g, 1) ≡ ite(g‘, f‘, 1)


Speicherbereinigung

•  Knoten sind Speicherblöcke ⇒ Referenzen–  Annahme: 22 Byte/Knoten ⇒ 32 Bytes werden

reserviert–  10 Byte Fragmentierung/Erhöhung Cache-Misses–  Wesentliche Inhalte sollten im Cache sein

•  Speicherorganisation (größere Blöcke anfordern)–  Zeiger für Verweise auf Knoten:

•  Bei der Initialisierung gilt „1“, bei „0“ kann gelöscht werden•  DDNode wird von BDDNode eingehüllt ⇒ id++ und id— !•  Overflow verhindern ⇒ Max. „65535“ erlaubt (2 Bytes)•  Kann dann nicht mehr gelöscht werden (Kompromiss)


Ausführung: BeispielManager manager(4, 521, 521);!BDDNode a( manager.createVariable(1) );!BDDNode b( manager.createVariable(2) );!BDDNode c( manager.createVariable(3) );!BDDNode d( manager.createVariable(4) );!BDDNode g = (a * b) ^ (!c | d);!BDDNode f = g.getCofactor( 1, ! BDDNode::getHighFactor() );!std::cout << f;!std::ofstream file("f.dot"); !manager.printNode(f, "f", file);!system("dot -o f.png -T png f.dot"); !manager.clear();!


•  Unittests (Referenzzähler, ...) •  CPPCheck (Bugs):

•  Speicherüberläufe •  Nullzeiger •  ...

Experimentelle Ergebnisse

•  SKs als Benchmarks von ISCAS’85–  ALUs, Addierer, Komparatoren und Multiplizierer–  Z. B. „C6288-16“ mit 2406 Gattern (Millionen Knoten)–  Ordnung: xn-1 < xn-2 < ... < yn-1 < yn-2 < ... < y0, wobei X

= Σi=0n-12ixi und Y = Σi=0

n-12iyi (gleich für jede Ausgabe), sonst Eingaben in der jeweiligen Reihenfolge

•  Testsystem (PC-Workstation mit macOS Sierra):–  Intel i5 2,4 GHz CPU, 3 MB Cache, 16 GB RAM–  Cache/Hashtabelle: m = 500.009 Knoten (Modulo)–  30 Minuten und jeweils 10 Versuche


Experimentelle Ergebnisse (2)Management der UT Multiplikations- und das Modulo-Verfahren (mit

Überläufern) sind sich bezüglich der Gleichverteilung von Knoten sehr ähnlich

Management der CT Cache mit Kollisionsstrategie benötigte ≈ 84,9 s (3 %) weniger als ein hashbasierter Cache, jedoch ≈ 827,2 MB (15 %) mehr Speicher (ohne CT nicht alle Berechnung möglich)

Komplementäre Kanten Mit CEs ≈ 777,5 MB (14 %) weniger und ein Zeitgewinn von 2.228,4 s (88 %)

Standardisierung Mit ST ≈ 269,1 MB (5 %) weniger und ein Zeitgewinn von 79,7 s (3 %)

Vergleich mit CUDD iBDD benötigte ≈ 59.121,6 MB (Faktor 3) und ≈ 17.254,5 s (Faktor 10) mehr


iBDD algorithmisch besser als originale Algorithmen von Bryant!

Mögliche Verbesserungen

•  Wenn die Kollisionsrate bei der UT zu hoch wird, dann diese dynamisch erweitern–  Rehashing, Limits

•  Bis 10% in der CT tot sind/Tabellen dynamisch erweitern

•  Wiederbelegung für Synthesen bzgl. der CT in O(1) möglich

•  Einsatz einer verketteten Liste•  Weniger interne Fragmentierung


Schluss

Danke für eure Aufmerksamkeit!


Efﬁziente Implementierung von Binären Entscheidungsdiagrammen · – Kombinationen zum gleichen...

Documents

Transcript of Efﬁziente Implementierung von Binären Entscheidungsdiagrammen · – Kombinationen zum gleichen...