DDDLIB is a library for manipulating formulae in a first-order logic over Boolean variables and inequalities of the form $x_1-x_2\le d$, where $x_1,x_2$ are real variables and $d$ is an integer constant. Formulae are represented in a semi-canonical data structure called difference decision diagrams (DDDs) which provide efficient algorithms for constructing formulae with the standard Boolean operators (conjunction, disjunction, negation, etc.), eliminating quantifiers, and deciding functional properties (satisfiability, validity and equivalence). The library is written in C and has interfaces for C++, Standard ML and Objective Caml.

References in zbMATH (referenced in 1 article , 1 standard article )

Showing result 1 of 1.
Sorted by year (citations)

  1. Møller, Jesper B.: DDDLIB: A library for solving quantified difference inequalities (2002)