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 :
Theses
Complete list of metadatas

Cited literature [113 references]  Display  Hide  Download

https://hal.univ-lorraine.fr/tel-01754359
Contributor : Thèses Ul <>
Submitted on : Friday, March 30, 2018 - 9:46:33 AM
Last modification on : Tuesday, April 24, 2018 - 1:30:09 PM

File

SCD_T_1998_0236_CASTRO.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : tel-01754359, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

78

Files downloads

81