Biddy  1.7.3
An academic Binary Decision Diagrams package
USER MANUAL

### TL;DR

Biddy is a multi-platform academic Binary Decision Diagrams package. It supports plain ROBDDs, ROBDDs with complemented edges, 0-sup-BDDs with complemented edges, and plain TZBDDs.

Biddy is capable of all the typical operations regarding Boolean functions and BDDs.

Biddy is a library to be included in your C and C++ projects:

1 #define UNIX
2 #define USE_BIDDY
3 #include "/path/to/biddy.h"

To compile Biddy library:

1 biddy> make dynamic
2 biddy> make clean

Dependencies:

When using Biddy on GNU/Linux, you may have to tell bash about the library:

1 export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:/absolute/path/to/biddy/library

There are two aditional packages included into Biddy distribution:

  • bddview is a pure Tcl/Tk script for visualization of BDDs,
  • BDD Scout is a demo application demonstrating the capability of Biddy and bddview.

Biddy is free software maintained by Robert Meolic (rober.nosp@m.t.me.nosp@m.olic@.nosp@m.um.s.nosp@m.i) at University of Maribor, Slovenia.

Homepage: http://biddy.meolic.com/

### 1. AN OVERVIEW

Biddy supports ROBDDs with complemented edges as described in "K. S. Brace, R. L. Rudell, R. E. Bryant. Efficient Implementation of a BDD Package. 27th ACM/IEEE DAC, pages 40-45, 1990".

Biddy supports 0-sup-BDDs with complemented edges as described in "S. Minato. Zero-Suppressed BDDs for Set Manipulation in Combinatorial Problems, 30th ACM/IEEE DAC, pages 272-277, 1993".

Biddy supports TZBDDs (tagged zero-supressed binary decison diagrams) as introduced by R. Meolic in 2016 (to be published).

Biddy includes:

  • automatic garbage collection with a system age (a variant of a mark-and-sweep approach),
  • node management through formulae protecting,
  • variable swapping and sifting algorithm (ROBDD, ZBDD, and TZBDD).

Biddy is optimized for efficiency, but it is mainly oriented towards readable and comprehensible source code in C.

Biddy is currently used in the following projects:

  • BDD Scout, demo project which allows visualization of BDDs and also includes some benchmarks
  • Efficient Symbolic Tools (EST), model checking and other algorithms for formal verification of systems (http://est.meolic.com/)

### 2. SOURCE CODE

Biddy is free software released under GPL.

The short name of Biddy package is 'biddy'. This name is placed in front of all filenames and external identifiers. It may appear in all lowercase, or with its first letter capitalized, written as 'biddy' and 'Biddy', respectively.

There are three categories of C functions.

  • Exported functions are visible outside the package.
  • Internal functions are visible to all files within the package.
  • Static functions are visible to the file only.

There are two types of C functions.

  • General functions which operates on a particular BDD and considering only graph properties (i.e. changing edge's mark, selecting nodes, counting nodes etc.). These functions are the same for different type of decision diagrams (BDD, ZDD, etc.). Functions, which add or delete nodes or those which needs info about variables (e.g. name) are not general functions. Exported general functions have prefix Biddy_.
  • Managed functions, which operates on a global properties of a BDD system (e.g. node table, variable table, formula table, various caches, etc.) or consider a BDD as a Boolean function (e.g. Boolean operations, counting minterms, etc.). These functions need info stored in a manager. Exported managed functions have prefix Biddy_Managed_.

Biddy consists of the following files:

There are two C headers, external and internal. The external header file, named biddy.h, defines features visible from outside the package. The internal header file, named biddyInt.h defines features used in multiple files inside the package, but not outside.

There are two aditional packages included into Biddy distribution:

  • bddview is a pure Tcl/Tk script for visualization of BDDs.
  • BDD Scout is a demo application demonstrating the capability of Biddy and bddview.

Details about building are given in Section 4.

### 3. USING BIDDY LIBRARY

Precompiled packages include dynamically linked library (i.e. *.so on GNU/Linux, *.dll on MS Windows, *.dylib on Mac OS X), and the appropriate C header biddy.h. Currently, there are no interfaces for other programming languages.

For linking with Biddy library you have to use:

1 -lbiddy -lgmp

Biddy is capable of all the typical operations regarding Boolean functions and BDDs.

The following code is an example of usage. Please note, that functions for node management are not shown. Moreover, Biddy has a manager but its usage is optional and it is also not shown in the given example.

IMPORTANT: You should define UNIX, MACOSX, or MINGW. You should define USE_BIDDY iff you are using Biddy via dynamic library.

1 #define UNIX
2 #define USE_BIDDY
3 #include "/path/to/biddy.h"
4 
5 #define Str2Var(x) (Biddy_GetVariable(Biddy_String)x)
6 
7 int main() {
8  Biddy_Edge f,g,h,r;
9 
10  Biddy_Init();
11 
12  f = Biddy_Eval1((Biddy_String)"(OR H E L L O)"); /* PREFIX INPUT */
13  g = Biddy_Eval1((Biddy_String)"(AND W O R L D)"); /* PREFIX INPUT */
14  h = Biddy_Eval2((Biddy_String)"~(H * E * L * L)"); /* INFIX INPUT */
15 
16  /* BASIC OPERATION */
17  r = Biddy_Xor(f,g);
18 
19  /* REPLACE SOME VARIABLES */
20  Biddy_ResetVariablesValue();
21  Biddy_SetVariableValue(Str2Var("H"),Biddy_FoaVariable((Biddy_String)"L"));
22  Biddy_SetVariableValue(Str2Var("K"),Biddy_FoaVariable((Biddy_String)"L"));
23  Biddy_SetVariableValue(Str2Var("W"),Biddy_FoaVariable((Biddy_String)"L"));
24  r = Biddy_Replace(r);
25 
26  /* SIMPLE RESTRICTION */
27  r = Biddy_Restrict(r,Str2Var("E"),Biddy_GetConstantZero());
28 
29  /* COUDERT AND MADRE'S RESTRICT FUNCTION */
30  r = Biddy_Simplify(r,h);
31 
32  /* SOME STATS */
33  printf("Function r depends on %u variables.\n",Biddy_VariableNumber(r));
34  printf("Function r has %.0f minterms.\n",Biddy_CountMinterm(r,0));
35  printf("BDD for function r has %u nodes.\n",Biddy_NodeNumber(r));
36 
37  /* TRUTH TABLE */
38  printf("Here is a truth table for function r\n");
39  Biddy_WriteTable(r);
40 
41  /* GRAPHVIZ/DOT OUTPUT */
42  Biddy_WriteDot("biddy.dot",r,"Function r");
43  printf("USE 'dot -y -Tpng -O biddy.dot' to visualize BDD for function r.\n");
44 
45  Biddy_Exit();
46 }

3.1 NODE MANAGEMENT THROUGH FORMULAE PROTECTING

Biddy includes powerful node management based on formulae tagging. There are six user functions to maintain nodes.

Biddy_AddFormula(name,bdd,c)

Nodes of the given BDD will be preserved for the given number of cleanings. If (name != NULL) then formula is accessible by its name. If formula with a given name already exists it is overwritten. If (c == 0) then formula is persistently preserved and you have to use Biddy_DeleteFormula to remove its nodes. There are two macros defined to simplify formulae management. Macro Biddy_AddTmpFormula(bdd,c) is defined as Biddy_AddFormula(NULL,bdd,c) and macro Biddy_AddPersistentFormula(name,bdd) is defined as Biddy_AddFormula(name,bdd,0).

Biddy_DeleteFormula(name)

Nodes of the given formula are tagged as not needed. Formula is not accessible by its name anymore. Regular cleaning with Biddy_Clean is not considered this tag.

Biddy_Clean()

Discard all nodes which were not preserved or which are not preserved anymore. Obsolete nodes are not immediately removed, they will be removed during the first garbage collection. Use Biddy_Purge or Biddy_PurgeAndReorder to immediately remove all non-preserved nodes.

Biddy_Purge()

Immediately remove all nodes which were not preserved or which are not preserved anymore. All formulae without name are deleted. Nodes from deleted prolonged formulae and nodes from deleted fortified formulae are removed if they are not needed by other formulae. Call to Biddy_Purge does not count as cleaning and thus all preserved formulae remains preserved for the same number of cleanings.

Biddy_PurgeAndReorder(bdd)

The same as Biddy_Purge but also trigger reordering on function (if BDD is given) or global reordering (if NULL is given). Reordering on function is currently supported only for ROBDDs.

Biddy_Refresh(bdd)

All obsolete nodes in the given bdd become fresh nodes. This is needed to implement user caches.

3.2. EXAMPLES OF NODE MANAGEMENT WITH BIDDY

The first example is a straightforward calculation.

1 f1 = op(...);
2 f2 = op(...);
3 g1 = op(f1,f2,...);
4 Biddy_AddTmpFormula(g1,1); /* g1 is preserved for next cleaning */
5 f1 = op(...);
6 f2 = op(...);
7 g2 = op(f1,f2,...);
8 Biddy_AddTmpFormula(g2,1); /* g2 is preserved for next cleaning */
9 Biddy_Clean(); /* g1 and g2 are still usable, f1 and f2 are obsolete */
10 result = op(g1,g2,...);
11 Biddy_AddPersistentFormula("result",result); /* final result is permanently preserved */
12 Biddy_Clean(); /* g1 and g2 are not needed, anymore */

If additional garbage collection is needed also after the calculation of g1, you can use the following code after the calculation of g1:

1 Biddy_AddTmpFormula(g1,2); /* g1 is preserved for next two cleanings */
2 Biddy_Clean(); /* g1 remains preserved for next cleaning */

In this approach, f1 and f2 become obsolete after Biddy_Clean, but their nodes are not immediately removed (automatic garbage collection is only started when there are no free nodes in the system). If garbage collection should be started immediately, you must use the following code after the calculation of g1:

1 Biddy_AddTmpFormula(g1,2); /* g1 is preserved for next two cleanings */
2 Biddy_Clean(); /* g1 remains preserved for next cleaning */
3 Biddy_Purge(); /* keep only preserved (g1) formulae */

Alternatively, you can use the following approach:

1 Biddy_AddTmpFormula(g1,1); /* g1 is preserved for next cleaning */
2 Biddy_Purge(); /* this will not make g1 obsolete */

To trigger reordering in this example, you should use Biddy_PurgeAndReorder to get the following code:

1 f1 = op(...);
2 f2 = op(...);
3 g1 = op(f1,f2,...);
4 Biddy_AddTmpFormula(g1,2); /* g1 is preserved for next two cleanings */
5 Biddy_PurgeAndReorder(NULL); /* keep only preserved formulae (g1), perform reordering */
6 Biddy_Clean(); /* g1 remains preserved for one additional cleaning */
7 f1 = op(...);
8 f2 = op(...);
9 g2 = op(f1,f2,...);
10 Biddy_AddTmpFormula(g2,1); /* g2 is preserved for next cleaning */
11 Biddy_PurgeAndReorder(NULL); /* keep only preserved formulae (g1, g2), perform reordering */
12 Biddy_Clean(); /* g1 and g2 are still usable but not preserved */
13 result = op(g1,g2,...);
14 Biddy_AddPersistentFormula("result",result); /* result is permanently preserved */
15 Biddy_PurgeAndReorder(NULL); /* keep only preserved formulae (result), perform reordering */

The second example is an iterative calculation:

1 f = op(...);
2 result = op(f,...);
3 while (!finish) {
4  Biddy_AddTmpFormula(result,1); /* result is preserved for next cleaning */
5  Biddy_Clean(); /* result is still usable but not preserved */
6  f = op(...);
7  g = op(f,...);
8  result = op(result,g,...);
9 }
10 Biddy_AddPersistentFormula("result",result); /* final result is permanently preserved */
11 Biddy_Clean(); /* temp results are not needed, anymore */

If garbage collection is needed also after the calculation of g, you must use the following code:

1 f = op(...);
2 result = op(f,...);
3 while (!finish) {
4  Biddy_AddTmpFormula(result,2); /* result is preserved for next two cleanings */
5  Biddy_Clean(); /* result remains preserved for one additional cleaning */
6  f = op(...);
7  g = op(f,...);
8  Biddy_AddTmpFormula(g,1); /* g is preserved for next cleaning */
9  Biddy_Clean(); /* result and g are still usable but not preserved */
10  result = op(result,g,...);
11 }
12 Biddy_AddPersistentFormula("result",result); /* final result is permanently preserved */
13 Biddy_Clean(); /* temp results are not needed, anymore */

To trigger reordering in the second example, you should change code in the following way:

1 f = op(...);
2 result = op(f,...);
3 while (!finish) {
4  Biddy_AddTmpFormula(result,2); /* result is preserved for next two cleanings */
5  Biddy_PurgeAndReorder(NULL); /* keep only preserved formulae (result), perform reordering */
6  Biddy_Clean(); /* result remains preserved for one additional cleaning */
7  f = op(...);
8  g = op(f,...);
9  Biddy_AddTmpFormula(g,1); /* g is preserved for next cleaning */
10  Biddy_Clean(); /* result and g are still usable but not preserved */
11  result = op(result,g,...);
12 }
13 Biddy_AddPersistentFormula("result",result); /* final result is permanently preserved */
14 Biddy_PurgeAndReorder(NULL); /* keep only preserved formulae (result), perform reordering */

The third example is an outline of an implementation of model checking where we are trying to benefit from regularly reordering:

1 sup = Prepare(...);
2 Biddy_AddPersistentFormula("sup",sup) /* sup is permanently preserved */
3 Z = 0;
4 last = 1;
5 while (Z!=last) {
6  Biddy_AddTmpFormula(Z,1); /* Z is preserved for next cleaning */
7  Biddy_PurgeAndReorder(NULL); /* keep only preserved formulae (sup,Z), perform reordering */
8  Biddy_Clean(); /* Z remains usable but not preserved */
9  last = Z;
10  Z = NextSet(Z,sup,...);
11 }
12 result = Z;
13 Biddy_AddPersistentFormula("result",result); /* final result is permanently preserved */
14 Biddy_DeleteFormula("sup"); /* optional, if you really need to remove sup */
15 Biddy_Purge(); /* optional, immediately remove non-preserved nodes */

The fourth example is an outline of an implementation of bisimulation where we are trying to benefit from regularly reordering:

1 init = AND(init_p,init_q)
2 Biddy_AddPersistentFormula("init",init) /* init is permanently preserved */
3 eq = InitialEq(init_p,tr_p,init_q,tr_q,...);
4 do {
5  Biddy_AddTmpFormula(eq,1); /* eq is preserved for next cleaning */
6  Biddy_PurgeAndReorder(NULL); /* keep only preserved formulae (init, eq), perform reordering */
7  Biddy_Clean(); /* eq remains usable but not preserved */
8  last = eq;
9  eq1 = NextEqPart1(eq,tr_p,tr_q,...);
10  eq2 = NextEqPart2(eq,tr_p,tr_q,...);
11  eq = AND(eq1,eq2);
12 } while (AND(init,eq)!=0 && eq!=last)
13 if (AND(init,eq)!=0) return false; else return true;
14 Biddy_DeleteFormula("init"); /* optional, if you really need to remove init */
15 Biddy_Purge(); /* optional, immediately remove non-preserved nodes */

The fifth example is an outline of an implementation of parallel composition where we are trying to benefit from intensive GC:

1 sacc = snew = AND(init_1,init_2,...,init_N);
2 for (i=1;i<=N;i++) di[i] = 0;
3 for (i=1;i<=N;i++) for (j=1;i<=N;j++) dij[i,j] = 0;
4 do {
5  Biddy_AddTmpFormula(snew,N*(N+1)); /* snew is preserved just long enough */
6  Biddy_AddTmpFormula(sacc,N*(N+1)); /* sacc is preserved just long enough */
7  new1 = 0;
8  for (i=1;i<=N;i++) {
9  sup = OneStep(snew,tr_i,...);
10  di[i] = OR(d[i],sup);
11  new1 = OR(new1,NextState(sup,...));
12  Biddy_AddTmpFormula(d[i],N*(N+1)); /* di[i] is preserved just long enough */
13  Biddy_AddTmpFormula(new1,1); /* new1 is preserved for next cleaning */
14  Biddy_Clean(); /* new1 remains usable but not preserved */
15  }
16  Biddy_AddTmpFormula(new1,N*N); /* new1 is preserved just long enough */
17  new2 = 0;
18  for (i=1;i<=N;i++) for (j=1;j<=N;j++) {
19  sup = OneStep(snew,tr_i,tr_j,...);
20  dij[i,j] = OR(d[i,j],sup);
21  new2 = OR(new2,NextState(sup,...);
22  Biddy_AddTmpFormula(dij[i,j],N*(N+1)); /* dij[i,j] is preserved just long enough */
23  Biddy_AddTmpFormula(new2,1); /* new2 is preserved for next cleaning */
24  Biddy_Clean(); /* new2 remains usable but not preserved */
25  }
26  snew = AND(OR(new1,new2),NOT(sacc));
27  sacc = OR(sacc,snew);
28 } while (snew!=0)
29 tr1 = 0;
30 for (i=1;i<=N;i++) {
31  sup = AddStab(di[i],...);
32  tr1 = OR(tr1,sup);
33  Biddy_AddTmpFormula(tr1,1); /* tr1 is preserved for next cleaning */
34  Biddy_Clean(); /* tr1 remains usable but not preserved */
35 }
36 Biddy_AddTmpFormula(tr1,N*N); /* tr1 is preserved just long enough */
37 tr2 = 0;
38 for (i=1;i<=N;i++) for (j=1;j<=N;j++) {
39  sup = AddStab(dij[i,j],...);
40  tr2 = OR(tr2,sup);
41  Biddy_AddTmpFormula(tr2,1); /* tr2 is preserved for next cleaning */
42  Biddy_Clean(); /* tr2 remains usable but not preserved */
43 }
44 result = OR(tr1,tr2);
45 Biddy_AddPersistentFormula("result",result); /* final result is permanently preserved */
46 Biddy_Clean(); /* temp results are not needed, anymore */

3.3 GARBAGE COLLECTION WITH A SYSTEM AGE

Garbage collection is automatically triggered if nodes from all reserved blocks of nodes are used. Garbage collection will remove as many obsolete nodes as possible.

Biddy does not use reference counter. We call the implemented algorithm "GC with a system age". It is a variant of a mark-and-sweep approach. Please note, that it relies on additional structure (Formula table).

Using system age instead of reference counter has some advantages. It allows GC to be started in any time without breaking the ongoing calculation. Thus, there is no need to taking care of repeating broken calculations. Moreover, the usage of system age instead of reference counter removes all the hassle of referencing and dereferencing nodes and thus it is favorable in an academic package oriented towards simple and readable source code.

There are four classes of nodes. Every node belongs to one of these classes:

  • fortified node (expiry value = 0);
  • fresh node (expiry value = biddySystemAge);
  • prolonged node (expiry value > biddySystemAge);
  • obsolete node (0 < expiry value < biddySystemAge).

Before GC, nodes must be refreshed in such a way that no successor of a non-obsolete node is obsolete. This can be achieved with relative simple loop which will check each node at least once.

There are three internal functions to maintain nodes.

  • BiddyProlongOne (one node is prolonged)
  • BiddyProlongRecursively (one node and its successors are prolonged recursively until a non-obsolete node is reached)
  • BiddyIncSystemAge (all fresh nodes become obsolete nodes)

There are four functions which can be used by an expert user.

  • Biddy_Garbage (explicite garbage collection call, removes all obsolete nodes)
  • Biddy_SwapWithLower (explicite swap of two variables, removes all obsolete and fresh nodes)
  • Biddy_SwapWithHigher (explicite swap of two variables, removes all obsolete and fresh nodes)
  • Biddy_Sifting (explicite sifting, removes all obsolete and fresh nodes)

These four functions will keep all nodes preserved by Biddy_AddFormula and they will not change the class of any node. Please note, that Biddy_Garbage can be started in any time whilst Biddy_SwapWithLower, Biddy_SwapWithHigher, and Biddy_Sifting will break an ongoing calculation (because they remove fresh nodes).

3.4 MORE DETAILS OF MEMORY MANAGEMENT (NODE CHAINING)

Biddy relies on a single hash table for all variables. However, it supports chaining of nodes to form different lists (using an extra pointer in each node). This facility is used to improve efficiency of garbage collection and sifting.

Please node, that node chaining is not determined or limited by using formulae protecting schema or a system age approach, it is an independent mechanism.

### 4. BUILDING PACKAGES

Compiling Biddy library

On GNU/Linux, we are using gcc.

1 biddy> make dynamic
2 biddy> make clean

Alternatively, you can use:

1 biddy> make static
2 biddy> make debug
3 biddy> make profile

You can use specify the target folder:

1 biddy> make dynamic "BINDIR = ./bin"
2 biddy> make clean "BINDIR = ./bin"

On MS Windows, we are using MSYS2. We use pacman to prepare the environment:

1 MSYS shell> pacman -Syuu
2 MSYS shell> pacman -S mingw-w64-i686-gcc
3 MSYS shell> pacman -S mingw-w64-x86_64-gcc
4 MSYS shell> pacman -S make
5 MSYS shell> pacman -S bison
6 MSYS shell> pacman -S gdb
7 MSYS shell> pacman -S nano
8 MSYS shell> pacman -S tar
9 MSYS shell> pacman -S subversion

Alternatively, you can use Visual Studio for building. There is a prepared solution consisting of many projects. You need to adapt include and lib folders.

1 ./VS/Biddy.sln

To produce nice setup files, we use Advanced Installer (http://www.advancedinstaller.com/). We have been granted a free licence. MANY THANKS!

Dependencies

On GNU/Linux, we are using libgmp (https://gmplib.org/).

On MS Windows, we are using MPIR library (http://mpir.org/).

Creating Biddy library as a zip package

1 biddy> ./package-bin

You need a zip program.

On MS Windows, you need 7-Zip (http://7-zip.org/) - and it has a strange use of -x! You also need file 7zsd_All_x64.sfx that you should download as part of "7z SFX Tools" from http://7zsfx.info/en/ and put in the directory containing 7z.exe.

You install the resulting package by extracting libraries to the appropriate directory (may be local, e.g. user's home directory).

When using this package on GNU/Linux, you have to tell bash about the library:

1 export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:/absolute/path/to/biddy/library

Creating zip file with source code of a complete Biddy project

1 biddy> ./package-source

If available, source code of bddview and BDD Scout will be included, too.

Creating packages for GNU/Linux

1 biddy> ./package-tgz
2 biddy> ./package-deb
3 biddy> ./package-rpm

These scripts are intedend to be used on Ubuntu. These scripts needs release number as an argument. Script package-tgz must be invoked before running package-deb. Debian packages must be created before RPM packages.

./package-tgz should create orig.tar.gz file and prepare directories for creating debian and RPM packages. You can run ./package-tgz only if version changes.

./package-deb should create debian packages (libbidy and libbiddy-dev). They are tested on Ubuntu system.

./package-rpm should create RPM packages (libbidy and libbiddy-devel). They are tested on openSUSE system.

Creating demo aplication bddscout

You need complete sources for biddy, bddview, and bddscout, Scripts are located in biddy/bddscout.

1 bddscout> ./package-bin
2 bddscout> ./package-tgz
3 bddscout> ./package-deb
4 bddscout> ./package-rpm

package-bin should create BDD Scout (staticaly linked with Biddy library). The script will produce a zip file. You install BDD Scout by simply unzip to the target directory.

./package-tgz should create orig.tar.gz file and prepare directories for creating debian and RPM packages. You can run ./package-tgz only if version changes.

./package-deb should create debian packages (bddscout, bddscout-bra, bddscout-ifip, bddscout-bddtrace, bddscout-ifip-data, and bddscout-bddtrace-data). They are tested on Ubuntu system.

./package-rpm should create RPM packages (bddscout, bddscout-bra, bddscout-ifip, bddscout-bddtrace, bddscout-ifip-data, and bddscout-bddtrace-data). They are tested on openSUSE system.

### 5. HISTORY

Biddy is based on a BDD package written in Pascal in 1992 as a student project. At that time, it was a great work and the paper about it won a second place at IEEE Region Student Paper Contest (Paris-Evry, 1993). The paper was published by IEEE as "A. Casar, R. Meolic. Representation of Boolean functions with ROBDDs. IEEE Student paper contest : regional contest winners 1990-1997 : prize-winning papers demonstrating student excellence worldwide, Piscataway, 2000" and can be obtained from http://research.meolic.com/papers/robdd.pdf

In 1995, this BDD package was rewritten in C. Later, this BDD package become an integral part of EST package, a prototype tool for formal verification of concurrent systems. The homepage for EST project is http://est.meolic.com/

In 2003, BDD package from EST was included in the report presented at 16th Symposium on Integrated Circuits and Systems Design (SBCCI'03). The report is available as a paper "G. Janssen. A Consumer Report on BDD Packages. IBM T.J. Watson Research Center. 2003". Get it from http://doi.ieeecomputersociety.org/10.1109/SBCCI.2003.1232832

In 2006, BDD package in EST got the name Biddy.

In 2007, a main part of Biddy package was extracted from EST forming a separate package called Biddy. The code has been reorganized in such a way, that EST is not using internal structures (e.g. node table) directly but using the provided API only.

In 2007, we created local svn repository for maintaining the source code (not live, anymore).

On May 15, 2008, Biddy v1.0 was released containing also bddview v0.95 (Tcl/Tk BDD viewer) and Bdd Scout v0.90 (demo application).

In 2009, 2010, and 2012 an updated version of Biddy v1.0 was released which added support for debian packaging, support for RPM packaging, fix error in Biddy_E and Biddy_A, and fix and improve details of documentation, packaging, and Tcl/Tk GUI.

In 2012, a research paper about Biddy library appears in Journal of Software (doi:10.4304/jsw.7.6.1358-1366) http://ojs.academypublisher.com/index.php/jsw/article/view/jsw070613581366/

In 2013, Biddy v1.1 was released. Biddy_Edge became a pointer instead of structure and all other structures were optimized.

In 2014, Biddy v1.2 was released. Variable swapping and sifting algorithm were the most significant additions.

In 2014, svn repositories for biddy, bddview and bddscout are moved to Savannah. http://svn.savannah.nongnu.org/viewvc/?root=biddy

In 2015, Biddy v1.3, v.1.4 and v1.5 was released. Various input/output methods have been added. Support for 64-bit arhitectures and support for Visual Studio projects were improved. Biddy got a manager. Many CUDD-like functions have been added. Comment's style changed to support doxygen. HTML and PDF documentation were produced.

Also in 2015, Personal Package Archive ppa:meolic/biddy has been created https://launchpad.net/~meolic/+archive/ubuntu/biddy

Also in 2015, sources became available on GitHub https://github.com/meolic/biddy

In 2016, Biddy v1.6 was released. Formulae are not recursively refreshed all the time. The size of Node table became resizable.

In 2017, Biddy v1.7 was released. Terminology is changed a lot, e.g. "formulae counter" is now "system age". Added support for 0-sup-BDDs and TZBDDs. Implemented creation and manipulaton of non-anonymous managers. Added manipulation of combination sets. Sifting does not require removing fresh nodes. Many new CUDD-like functions have been added. bddview and BDD Scout have been significantly improved.

### 6. PUBLICATIONS

If you find our work useful, please, cite us.