Combination of Boxes and Polyhedra Abstractions for Constraint Solving

Ghiles Ziat (1) , Alexandre Maréchal (2, 1) , Marie Pelleau (3) , Antoine Miné (1, 4) , Charlotte Truchet (5, 6)

1 APR - Algorithmes, Programmes et Résolution
2 VERIMAG - IMAG - VERIMAG
3 I3S - Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis
4 IUF - Institut universitaire de France
5 LS2N - Laboratoire des Sciences du Numérique de Nantes
6 LS2N - équipe TASC - Théorie, Algorithmes et Systèmes en Contraintes

This paper investigates the use of abstract domains from Abstract Interpretation (AI) in the field of Constraint Programming (CP). CP solvers are generally very efficient on a specific constraint language, but can hardly be extended to tackle more general languages, both in terms of variable representation (discrete or continuous) and constraint type (global, arithmetic, etc.). For instance, linear constraints are usually solved with linear programming techniques, but non-linear ones have to be either linearized, reformulated or sent to an external solver. We approach this problem by adapting to CP a popular domain construction used to combine the power of several analyses in AI: the reduced product. We apply this product on two well-known abstract domains, Boxes and Polyhedra, that we lift to constraint solving. Finally we define general metrics for the quality of the solver results, and present a benchmark accordingly. Experiments show promising results and good performances.

Domaines: Informatique [cs]; Autre [cs.OH]

Ghiles Ziat, Alexandre Maréchal, Marie Pelleau, Antoine Miné, Charlotte Truchet. Combination of Boxes and Polyhedra Abstractions for Constraint Solving. The 8th International Workshop on Numerical and Symbolic Abstract Domains - NSAD 2019, Oct 2019, Porto, Portugal. pp.119--135, ⟨10.1007/978-3-030-54997-8_8⟩. ⟨hal-02457083⟩