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.
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
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.