Constraint programming aims at solving hard combinatorial problems, with computation times increasing exponentially in practice. Today the methods are efficient enough to solve large industrial problems within a generic framework. However, solvers are dedicated to a single variable type: integer or real. Solving mixed problems relies on ad hoc transformations. In another field, abstract interpretation offers tools to prove program properties, by studying an abstraction of their concrete semantics, that is, the set of possible values of the variables during an execution.
Various representations for these abstractions have been proposed – they are known as abstract domains. Abstract domains can mix any type of variable and even represent relations between different variables. In this work, the author defines abstract domains for constraint programming, so as to create a generic problem-solving method, dealing with both integers and real variables.
The octagon abstract domain is also investigated, already defined in abstract interpretation. Guiding the search by the octagonal relations, a set of good results are presented on a continuous benchmark. The author also defines their solving method using Abstract Interpretation techniques, in order to include existing abstract domains. The solver, AbSolute, is able to solve mixed problems and use relational domains.
1. State of the Art
2. Abstract Interpretation for Constraint Programming
3. Octagons
4. Octagonal Solving
5. An Abstract Solver : AbSolute
Marie Pelleau is a Doctorate in Computer Science at the University of Nantes, France. Her research interests include Constraint Programming and local search Constraint Programming (CP) to model and solve combinatory problems.