jinc_symbol

JINC is an object-oriented binary decision diagram (BDD) library written in C++. The main intention while developing JINC was to design a simple to use API. The clean design of JINC makes it also easy to implement new variants and run-time and space-efficent (which has been shown in several case studies).

JINC offers a wide range of features which haven't been implemented elsewhere. It is the first OBDD library to make use of modern multi-threading architectures. The novel reordering system speeds up the reordering algorithms without changing their implementation. JINC automatically identifies swap operations which can be performed in parallel. It also provides mechanisms to reduce the memory footprint by several factors by eliminating temporary node creation for complex calculations. In some
benchmarks it has been shown that JINC (even without using its multi-threading algorithms) is faster than the well established OBDD library CUDD.

JINC provides:

  • several OBDD variants (ADDs, NADDs, ZADDs, TADDs, ...)

  • support for multi-variable variants (MDDs)

  • run-time efficient multi-threading approaches

  • space-efficient multi-operand APPLY algorithm

  • novel reordering template system

  • iterator concept

  • clean API

  • speed

  • ...


JINC is based on a solid theoretical framework (see
publication section for more details). Besides that it uses state of the art programming techniques to create a fast, reliable and easy to use OBDD library.

A short introduction in JINC can be found in the
tutorial section. If you have questions, remarks or comments feel free to contact me. Feedback is always welcome.