Generating Propagation Rules for Finite Domains via Unification in Finite Algebras
Résumé
Constraint solving techniques are nowadays frequently based on constraint propagation which can be interpreted as a specific form of deduction. Using constraint programming languages enhanced with constraint handling rules facilities, we can now perform constraint propagation just by applying deduction rules over constraints. The idea of computing propagation rules in the particular case of small finite domains has emerged in a recent paper by K. R. Apt and E. Monfroy [1]. Due to its interest for practical applications, the integration of Finite Domains into (constraint) logic programming has been thoroughly investigated during the last decade. A possible way of integration is achieved using a unitary unification algorithm, based on the handling of Directed Acyclic Graphs to represent functions over the finite domain. We show in this paper the interest of this solver for the generation of propagation rules for finite domains. Our motivation relies on the well-established fact that unification provides a concise solution to perform safe deductions about the possible values taken by variables. Conversely, the propagation rules appear to be a quite interesting output in comparison with the symbolic most general solution usually printed out by the unification algorithm. Therefore, a rule-based approach and the notion of propagation rules are adopted here, in order to provide a more understandable output to the unification algorithm.