Release of ocplib-simplex, version 0.5

Authors: Steven de Oliveira, Pierre Villemot, Hichem Rami Ait El Hara, Guillaume Bury

Date: 2023-01-05

Category: Formal Methods

Tags: OCaml, alt-ergo, simplex, ocplib

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:

• Make the library's API more generic and easier to use (see the System Solving Example or the Linear Optimization Example);

• All the modules are better documentated in their .mli interfaces (see coreSig.mli for example);

• the build system has been switched to dune

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: alt-ergo@ocamlpro.com.

About Alt-Ergo

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 Why3 platform. Its development started in 2006 at the Laboratoire de Recherche en Informatique (LRI - CNRS/Inria) of the Université Paris-Saclay and is maintained, developed and distributed since 2013 by the Formal Methods team at OCamlPro.

This work is made possible through research projects like Décysif, Soprano, BWare, Vocal and LCHIP, as well as support from our Alt-Ergo Users' Club members. If Alt-Ergo has been valuable to you, consider joining the Alt-Ergo Users' Club.