Release of ocplib-simplex, version 0.5
On last November, we released version 0.5 of ocplib-simplex, a generic library implementing the Simplex Algorithm in OCaml. It is a key component of the Alt-Ergo automatic theorem prover that we keep developing at OCamlPro.
The simplex algorithm⚓
The Simplex Algorithm is well known among linear optimization enthusiasts. Let's say you own a manufacture producing two kinds of chairs: the first is cheap, you make a small profit out of them but they are quick to produce; the second one is a bit more fancy, you make a bigger profit but they need a lot of time to build. You have a limited amount of wood and time. How many cheap and fancy chairs should you produce to optimize your profits?
You can represent this problem with a set of mathematical constraints (more precisely, linear inequalities) which is precisely the scope of the simplex algorithm. Given a set of linear inequalities, it computes a solution maximizing a given value (in our example, the total profit). If you are interested in the detail of the algorithm, you shoud definitely watch this video.
The simplex algorithm is known to be a difficult problem in terms of complexity. While the base algorithm is EXP-time, it is generally very efficient in practice.
What Changed in 0.5 ?⚓
Among the main changes in this new version of ocplib-simplex:
All the modules are better documentated in their
.mliinterfaces (see coreSig.mli for example);
the build system has been switched to
We hope that this work of simplification will help you to integrate this library more easily in your projects!
If you want to follow this project, report an issue or contribute, you can find it on GitHub.
Please do not hesitate to contact us at OCamlPro: firstname.lastname@example.org.
Alt-Ergo is an open-source automatic solver of mathematical formulas designed for program verification. Alt-Ergo is very successful for proving formulas generated in the context of deductive program verification. It was originally designed and tuned to be used by the Why playform. Its development started in 2006 at the Laboratoire de Recherche en Informatique (LRI) of the Université Paris Sud and is maintained, developed and distributed since 2013 by the company OCamlPro.
Alt-Ergo is part of the formal method team here at OCamlPro. This work is partially funded by the research projects Soprano, BWare, Vocal and LCHIP. If you like Alt-Ergo, consider joining the Alt-Ergo user’s Club