Combination of Boxes and PolyhedraAbstractions for Constraint Solving

EasyChair Preprint 1906

Abstract

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 \emph{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.

Keyphrases: Constraint Programming, Reduced Products, abstract domains, abstract interpretation, propagation

@booklet{EasyChair:1906,
  author    = {Ghiles Ziat and Alexandre Maréchal and Marie Pelleau and Antoine Miné and Charlotte Truchet},
  title     = {Combination of Boxes and PolyhedraAbstractions for Constraint Solving},
  howpublished = {EasyChair Preprint 1906},
  year      = {EasyChair, 2019}}