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 and others 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|
| || Interval constraints (||None|| Simple Cartesian product of variable domains. |
| || Propositional formula (||Conflict driven clause learning||Based on Minisat. This domain is experimental (and probably bugged!).|
| || Logic difference constraints (||Incremental Floyd-Warshall algorithm|| |
In addition, new abstract domains can be derived from existing ones using abstract transformers.
|Abstract transformers||Constraint language||Propagation||Description|
| || Union of ||Component-wise propagation of each subdomains.||In addition to the classical direct product of abstract interpretation, it has some facilities for transformers that shares subdomains.|
| || Quantifier-free logic formula where predicates are constraints in || Based on the entailment of constraint in || Equip an abstract domain |
| || Arithmetic constraints, functions (||HC4 algorithm|| Equip an abstract domain |
| || Union of || Transfer over-approximation ||Can be used to transfer non-linear constraints to a linear solver whenever the non-linear variables are instantiated.|
| ||None|| Propagation loop of the propagators in || Meta abstract domain, computing the closure of |
In addition, each domain is equipped with numerous splitting strategies that can impact the performance.
What to expect next?
A linear programming solver such as VPL, or the one of Apron should be added. The next big step is to integrate ideas from abstract conflict driven learning (ACDL) to support conflicts learning.
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.