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.

Binary decision diagrams (BDD)

In computer science, a binary decision diagram (BDD) or branching program is a data structure that is used to represent a Boolean function. On a more abstract level, BDDs can be considered as a compressed representation of sets or relations. Unlike other compressed representations, operations are performed directly on the compressed representation, i.e. without decompression. Other data structures used to represent Boolean functions include negation normal form (NNF), Zhegalkin polynomials, and propositional directed acyclic graphs (PDAG). ~ Wikipedia, 09/10/2020

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