Hello! You reached the
AbSolute is a constraint solver written in OCaml for research purposes, but we hope that it can be used outside of research as well!
The main originality of this solver is to be based on abstract interpretation, which is a field studying static analysis of programs.
We have discovered similitudes between constraint programming and abstract interpretation at the theoretical level, and this solver is a practical experimentation of these findings.
In this book, you will learn how to install AbSolute and how to solve your own constraint problems.
We also include a guide to kobe which is a benchmarking tool with support for AbSolute and other solvers.
For adventurous users, we provide a guide for contributing to Absolute, as well as some notes about the research relevant to this project.
This project is available on github.
Highlight of AbSolute features
An abstract domain encapsulates a solver for a specific constraint language.
We summarize the supported abstract domains in the table below (
c1,c2 are constraints,
X,Y variables and
Each abstract domain is parametrized by a bound type
Q if it contains variables over integers, floating point numbers or rational.
|Abstract domain||Constraint language||Propagation||Description|
| || Arithmetic constraints, functions (||HC4 algorithm, propagation loop|| |
| || Box constraint and reified constraint of the form (|| Same as || |
| || Logic difference constraints (||Incremental Floyd-Warshall algorithm|
| || Box and octagon constraints with equivalence constraints (||Bridge between box and octagon domains when they are defined on disjoint set of variables.|
In addition, each domain is equipped with numerous splitting strategies that can impact the performance.
What to expect next?
We currently work on integrating a SAT solver, integrating back some features from the initial version of AbSolute such as support for linear programming through VPL and Apron library, and reduced product to combine domains.
We have several projects relevant to AbSolute that are worth checking out:
- kobe: Constraint benchmarking tools suite. It is described in more depth in the benchmarking chapter.
- minisatml: SAT solver based on MiniSAT, note that this project is a library not directly executable.
- ptal.github.io: The repository hosting this book.
- solvers-opam: The OPAM packages repository containing libraries and executables surrounding constraint solving.