AbSolute

AbSolute is a constraint solver based on abstract domains. The source code is available on GitHub.

The first draft of this solver has been published:

• Marie Pelleau, Antoine Miné, Charlotte Truchet, Frédéric Benhamou, Constraint Solver based on Abstract Domains, 14th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), Rome, Italie, 2013 [Article] [Bibtex]

This solver can solve continous problems, discrete problems, but also mixed problems (containing both discrete and continuous variables). The following picture shows the obtained solutions for the same problem depending on the variable types. The first disc has 2 continuous variables, the second 1 discrete and 1 continuous variable, the last one, 2 discrete variables.

AbSolute uses Apron, an Ocaml library for abstract domains, one can thus solve problems using abstract domains other than intervals. The following picture shows solutions obtained for a problem corresponding to the intersection of two discs, using intervals (classic solver) on one side, and with octagons on the other side.

Finally, abstract domains can also correspond to a product of abstract domains. The following picture compares solutions obtained with the intervals to the ones obtained to the product of intervals and polyhedra.