Краткое описание

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
• 
  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";;

Лицензирование

Я, владелец авторских прав на это произведение, добровольно публикую его на условиях следующих лицензий:

Разрешается копировать, распространять и/или изменять этот документ в соответствии с условиями GNU Free Documentation License версии 1.2 или более поздней, опубликованной Фондом свободного программного обеспечения, без неизменяемых разделов, без текстов, помещаемых на первой и последней обложке. Копия лицензии включена в раздел, озаглавленный GNU Free Documentation License.http://www.gnu.org/copyleft/fdl.htmlGFDLGNU Free Documentation Licensetruetrue

	Этот файл доступен по лицензии Creative Commons Attribution-Share Alike 3.0 Unported.
	Вы можете свободно: делиться произведением – копировать, распространять и передавать данное произведение создавать производные – переделывать данное произведение При соблюдении следующих условий: атрибуция – Вы должны указать авторство, предоставить ссылку на лицензию и указать, внёс ли автор какие-либо изменения. Это можно сделать любым разумным способом, но не создавая впечатление, что лицензиат поддерживает вас или использование вами данного произведения. распространение на тех же условиях – Если вы изменяете, преобразуете или создаёте иное произведение на основе данного, то обязаны использовать лицензию исходного произведения или лицензию, совместимую с исходной.
	Этот признак лицензирования был добавлен к этому файлу как часть обновления лицензии GFDL.http://creativecommons.org/licenses/by-sa/3.0/CC BY-SA 3.0Creative Commons Attribution-Share Alike 3.0truetrue

Этот файл доступен по лицензии Creative Commons Attribution-Share Alike 2.5 Generic

Вы можете свободно:

• делиться произведением – копировать, распространять и передавать данное произведение
• создавать производные – переделывать данное произведение

При соблюдении следующих условий:

• атрибуция – Вы должны указать авторство, предоставить ссылку на лицензию и указать, внёс ли автор какие-либо изменения. Это можно сделать любым разумным способом, но не создавая впечатление, что лицензиат поддерживает вас или использование вами данного произведения.
• распространение на тех же условиях – Если вы изменяете, преобразуете или создаёте иное произведение на основе данного, то обязаны использовать лицензию исходного произведения или лицензию, совместимую с исходной.

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

Вы можете выбрать любую из этих лицензий.