HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Une approche déductive de la résolution de problèmes de satisfaction de contraintes

Abstract : In this thesis, we model the resolution of constraint satisfaction problems (CSPs) as a deductive process. We formalise CSP solving techniques over finite domains using rewrite rules and strategies. The rules express the transformations over the set of constraints carried out by these techniques. The strategies control the application of these rules. This approach allows us to easily verify properties like correctness, completeness, and termination of a solver. The use of a powerful strategy language allows us to describe heuristics in an abstract and flexible way. Furthermore, using this deductive approach we can justify the existence or absence of a solution: we just have to look at the proof term in order to reconstruct exactly a proof of the computation carried out. To validate our approach, we have implemented the system COLETTE using the ELAN language. Firstly, we study the resolution of a set of elementary constraints combined by conjunction operators. Next, we focus on the resolution of optimisation problems using CSP solving techniques. Then, we extend the constraint language in order to consider the combination of elementary constraints by the logical operators of disjunction, implication, and equivalence. The treatment of disjunctive constraints is described in detail. Finally, we study the cooperation of solvers. Using the concurrent strategy operators of the ELAN language we describe in an abstract way some schemes of sequential and concurrent cooperation. For other types of cooperation, we use low-level primitives for process communication available in ELAN.
Document type :
Complete list of metadata

Cited literature [113 references]  Display  Hide  Download

Contributor : Thèses Ul Connect in order to contact the contributor
Submitted on : Friday, March 30, 2018 - 9:46:33 AM
Last modification on : Saturday, October 16, 2021 - 11:26:09 AM


Files produced by the author(s)


  • HAL Id : tel-01754359, version 1



Carlos Castro. Une approche déductive de la résolution de problèmes de satisfaction de contraintes. Autre [cs.OH]. Université Henri Poincaré - Nancy 1, 1998. Français. ⟨NNT : 1998NAN10236⟩. ⟨tel-01754359⟩



Record views


Files downloads