reduced-ordered-binary-decision-diagrams: ROBDDs for JS

This library implements a basic structure for reduced ordered binary decision diagrams, and Boolean operations to compose them.

A binary decision diagram (BDD) is a data structure used to represent Boolean functions. Conceptually, a BDD is a directed graph where sink nodes represent truth- or falsehood. At each node a decision is made about the value of the binary variable whose label is associated with that node.

A BDD is called reduced when the BDD is minimal with respect to the following reduction rules:

• Given two nodes with the same variable label, same true-path and same false-path, one of them can be replaced.
• Given a node whose true-path and false-path coincide, the node can be removed.

A BDD is called ordered when, for each path from the source to a sink node, the labels encountered follow the same ordering (though not every variable needs to occur in each path).

The variable ordering is determined upon instantiation.

Installation

npm i reduced-ordered-binary-decision-diagrams

Example

const { ROBDD } = require('reduced-ordered-binary-decision-diagrams')

const x = ROBDD.variable()
const y = ROBDD.variable()

console.warn(ROBDD.or(x, y))

Future plans

None, currently