BDD graph for the Boolean formula x1 * x2 + x3 * x4 + x5 * x6 + x7 * x8 using a bad variable ordering
Visualization of the BDD for the Boolean formula x1 * x2 + x3 * x4 + ... + x19 * x20 using a bad variable ordering
The following is the RML (Relational Manipulation Language) code that I fed to CrocoPat
to produce the GraphViz dot files:
// RML program to generate BDD graphs for the formula
// x1 & x2 | x3 & x4 | x5 & x6 | x7 & x8,
// using two different variable orderings.
// "crocopat -e BDD_Variable_Ordering.rml" generates two files in dot format.
// "dot -Tsvg BDD_Variable_Ordering_Bad.dot -o BDD_Variable_Ordering_Bad.svg"
// generates a file in SVG format from the file in dot format.
// There are two ('Boolean') values for the variables x1, ..., x8.
DOM("0");
DOM("1");
// F is the name of the Boolean formula.
F(x1,x2,x3,x4,x5,x6,x7,x8) := (x1="1" & x2="1")
| (x3="1" & x4="1")
| (x5="1" & x6="1")
| (x7="1" & x8="1");
// Prints the BDD as graph in GraphViz dot format,
// using a good variable ordering resulting in linear size of the graph.
PRINT GRAPH( F(x1,x2,x3,x4,x5,x6,x7,x8) )
TO "BDD_Variable_Ordering_Good.dot";
// Prints the BDD as graph in GraphViz dot format,
// using a bad variable ordering resulting in exponential size of the graph.
// The first term of the conjunction sets the variable ordering.
PRINT GRAPH( TRUE(x1,x3,x5,x7,x2,x4,x6,x8) &
F(x1,x2,x3,x4,x5,x6,x7,x8) )
TO "BDD_Variable_Ordering_Bad.dot";;
Licentie
Ik, de auteursrechthebbende van dit werk, maak het hierbij onder de volgende licenties beschikbaar:
Toestemming wordt verleend voor het kopiëren, verspreiden en/of wijzigen van dit document onder de voorwaarden van de GNU-licentie voor vrije documentatie, versie 1.2 of enige latere versie als gepubliceerd door de Free Software Foundation; zonder Invariant Sections, zonder Front-Cover Texts, en zonder Back-Cover Texts. Een kopie van de licentie is opgenomen in de sectie GNU-licentie voor vrije documentatie.http://www.gnu.org/copyleft/fdl.htmlGFDLGNU Free Documentation Licensetruetrue
Delen – het werk kopiëren, verspreiden en doorgeven
Remixen – afgeleide werken maken
Onder de volgende voorwaarden:
naamsvermelding – U moet op een gepaste manier aan naamsvermelding doen, een link naar de licentie geven, en aangeven of er wijzigingen in het werk zijn aangebracht. U mag dit op elke redelijke manier doen, maar niet zodanig dat de indruk wordt gewekt dat de licentiegever instemt met uw werk of uw gebruik van zijn werk.
Gelijk delen – Als u het werk heeft geremixt, veranderd, of erop heeft voortgebouwd, moet u het gewijzigde materiaal verspreiden onder dezelfde licentie als het oorspronkelijke werk, of een daarmee compatibele licentie.
Deze licentietag is toegevoegd aan dit bestand in verband met de GFDL licentie-update.http://creativecommons.org/licenses/by-sa/3.0/CC BY-SA 3.0Creative Commons Attribution-Share Alike 3.0truetrue
Delen – het werk kopiëren, verspreiden en doorgeven
Remixen – afgeleide werken maken
Onder de volgende voorwaarden:
naamsvermelding – U moet op een gepaste manier aan naamsvermelding doen, een link naar de licentie geven, en aangeven of er wijzigingen in het werk zijn aangebracht. U mag dit op elke redelijke manier doen, maar niet zodanig dat de indruk wordt gewekt dat de licentiegever instemt met uw werk of uw gebruik van zijn werk.
Gelijk delen – Als u het werk heeft geremixt, veranderd, of erop heeft voortgebouwd, moet u het gewijzigde materiaal verspreiden onder dezelfde licentie als het oorspronkelijke werk, of een daarmee compatibele licentie.
== Summary == {{Information| |Description = BDD graph for the Boolean formula x1 * x2 + x3 * x4 + x5 * x6 + x7 * x8 using a good variable ordering |Source = self-made using CrocoPat, a tool for relational programming, and GraphViz dot, a tool for graph la