Library of Efficient Data types and Algorithms

The Library of Efficient Data types and Algorithms (LEDA) is a proprietarily-licensed software library providing C++ implementations of a broad variety of algorithms for graph theory and computational geometry. It was originally developed by the Max Planck Institute for Informatics Saarbrücken. Since 2001, LEDA is further developed and distributed by the Algorithmic Solutions Software GmbH.

LEDA is available as Free, Research, and Professional edition. The Free edition is freeware, with source code access available for purchase. The Research and Professional editions require payment of licensing fees for any use. Since October 2017, LEDA graph algorithms are also available for Java development environment.

Technical details

Data types

Numerical representations

LEDA provides four additional numerical representations alongside those built-in to C++: integer, rational, bigfloat, and real:

• LEDA's integer type offers an improvement over the built-in int datatype by eliminating the problem of overflow at the cost of unbounded memory usage for increasingly large numbers.
• It follows that LEDA's rational type has the same resistance to overflow because it is based directly on the mathematical definition of rational as the quotient of two integers.
• The bigfloat type improves on the C++ floating-point types by allowing for the significand (also commonly called mantissa) to be set to an arbitrary level of precision instead of following the IEEE standard.
• LEDA's real type allows for precise representations of real numbers, and can be used to compute the sign of a radical expression.

Error checking

LEDA makes use of certifying algorithms to demonstrate that the results of a function are mathematically correct. In addition to the input and output of a function, LEDA computes a third "witness" value which can be used as an input to checker programs to validate the output of the function. LEDA's checker programs were developed in Simpl, an imperative programming language, and validated using Isabelle/HOL, a software tool for checking the correctness of mathematical proofs.

The nature of a witness value often depends on the type of mathematical calculation being performed. For LEDA's planarity testing function, If the graph is planar, a combinatorial embedding is produced as a witness. If not, a Kuratowski subgraph is returned. These values can then be passed directly to checker functions to confirm their validity. A developer only needs to understand the inner-workings of these checker functions to be confident that the result is correct, which greatly reduces the learning curve compared to gaining a full understanding of LEDA's planarity testing algorithm.

Use cases

LEDA is useful in the field of computational geometry due to its support for exact representations of real numbers via the leda_real datatype. This provides an advantage in accuracy over floating-point arithmetic. For example, calculations involving radicals are considerably more accurate when computed using leda_real. Algorithms such as parametric search, a technique for solving a subset of optimization problems, and others under the real RAM model of computation rely upon real number parameters to produce accurate results.

Alternatives

Boost and LEMON are potential alternative libraries with some benefits in efficiency due to different implementations of fundamental algorithms and data structures. However, neither employs a similar set of correctness checking, particularly when dealing with floating-point arithmetic.

External links

• Official website