Beschreibung

The PNG picture is 518 x 32 pixel.

Other BDD pictures for similar formulas:

• 
  BDD graph for the Boolean formula x1 * x2 + x3 * x4 + x5 * x6 + x7 * x8 using a good variable ordering
• 
  BDD graph for the Boolean formula x1 * x2 + x3 * x4 + x5 * x6 + x7 * x8 using a bad variable ordering

The following is the RML (Relational Manipulation Language) code that I fed to CrocoPat to produce the dat files for VisuBDD:

// RML program to generate BDD visualizations for the formula
// x1 & x2 | x3 & x4 | ... | x19 & x20,
// using two different variable orderings.
// "crocopat -e BDD_Variable_Ordering_VisuBDD.rml" 
// generates two files in dat format.
// "java -classpath <your_CrocoPat_dir> 
//  VisuBDD.VisualizeSize  BDD_Variable_Ordering_VisuBDD_Bad.dat"
// displays a visualization of the BDD graph on screen.

// There are two ('Boolean') values for the variables x1, ..., x20.
DOM("0");
DOM("1");

// F is the name of the Boolean formula.
F(x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20) := 
                               (x1="1" & x2="1") 
                             | (x3="1" & x4="1")
                             | (x5="1" & x6="1")
                             | (x7="1" & x8="1")
                             | (x9="1" & x10="1") 
                             | (x11="1" & x12="1")
                             | (x13="1" & x14="1")
                             | (x15="1" & x16="1")
                             | (x17="1" & x18="1")
                             | (x19="1" & x20="1");

// Prints the number of nodes per variable in dat format for VisuBDD,
// using a good variable ordering resulting in linear size of the graph.
PRINT NODESPERVAR( F(x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20) ) 
      TO "BDD_Variable_Ordering_VisuBDD_Good.dat";

// Prints the number of nodes per variable in dat format for VisuBDD,
// using a bad variable ordering resulting in exponential size of the graph.
// The first term of the conjunction sets the variable ordering.
PRINT NODESPERVAR( TRUE(x1,x3,x5,x7,x9,x11,x13,x15,x17,x19,x2,x4,x6,x8,x10,x12,x14,x16,x18,x20) &
                   F(x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20) ) 
      TO "BDD_Variable_Ordering_VisuBDD_Bad.dat";;

Lizenz

Ich, der Urheberrechtsinhaber dieses Werkes, veröffentliche es hiermit unter der folgenden Lizenz:

Es ist erlaubt, die Datei unter den Bedingungen der GNU-Lizenz für freie Dokumentation, Version 1.2 oder einer späteren Version, veröffentlicht von der Free Software Foundation, zu kopieren, zu verbreiten und/oder zu modifizieren; es gibt keine unveränderlichen Abschnitte, keinen vorderen und keinen hinteren Umschlagtext. Der vollständige Text der Lizenz ist im Kapitel GNU-Lizenz für freie Dokumentation verfügbar.http://www.gnu.org/copyleft/fdl.htmlGFDLGNU Free Documentation Licensetruetrue

	Diese Datei ist unter der Creative-Commons-Lizenz „Namensnennung – Weitergabe unter gleichen Bedingungen 3.0 nicht portiert“ lizenziert.
	Dieses Werk darf von dir verbreitet werden – vervielfältigt, verbreitet und öffentlich zugänglich gemacht werden neu zusammengestellt werden – abgewandelt und bearbeitet werden Zu den folgenden Bedingungen: Namensnennung – Du musst angemessene Urheber- und Rechteangaben machen, einen Link zur Lizenz beifügen und angeben, ob Änderungen vorgenommen wurden. Diese Angaben dürfen in jeder angemessenen Art und Weise gemacht werden, allerdings nicht so, dass der Eindruck entsteht, der Lizenzgeber unterstütze gerade dich oder deine Nutzung besonders. Weitergabe unter gleichen Bedingungen – Wenn du das Material wiedermischst, transformierst oder darauf aufbaust, musst du deine Beiträge unter der gleichen oder einer kompatiblen Lizenz wie das Original verbreiten.
	Diese Lizenzmarkierung wurde auf Grund der GFDL-Lizenzaktualisierung hinzugefügt.http://creativecommons.org/licenses/by-sa/3.0/CC BY-SA 3.0Creative Commons Attribution-Share Alike 3.0truetrue

Diese Datei ist unter der Creative-Commons-Lizenz „Namensnennung – Weitergabe unter gleichen Bedingungen 2.5 generisch“ (US-amerikanisch) lizenziert.

Dieses Werk darf von dir

• verbreitet werden – vervielfältigt, verbreitet und öffentlich zugänglich gemacht werden
• neu zusammengestellt werden – abgewandelt und bearbeitet werden

Zu den folgenden Bedingungen:

• Namensnennung – Du musst angemessene Urheber- und Rechteangaben machen, einen Link zur Lizenz beifügen und angeben, ob Änderungen vorgenommen wurden. Diese Angaben dürfen in jeder angemessenen Art und Weise gemacht werden, allerdings nicht so, dass der Eindruck entsteht, der Lizenzgeber unterstütze gerade dich oder deine Nutzung besonders.
• Weitergabe unter gleichen Bedingungen – Wenn du das Material wiedermischst, transformierst oder darauf aufbaust, musst du deine Beiträge unter der gleichen oder einer kompatiblen Lizenz wie das Original verbreiten.

https://creativecommons.org/licenses/by-sa/2.5CC BY-SA 2.5 Creative Commons Attribution-Share Alike 2.5 truetrue

Du darfst es unter einer der obigen Lizenzen deiner Wahl verwenden.