Reseña: Solveurs CP(FD) vérifiés formellement
Se ha publicado un artículo de razonamiento formalizado en Coq sobre restricciones titulado Solveurs CP(FD) vérifiés formellement.
Sus autores son Catherine Dubois y Arnaud Gotlieb.
El trabajo se ha presentado en las 9èmes Journées Francophones de Programmation par Contraintes.
Su resumen es
Constraint solvers are used to solve problems coming from optimization, scheduling, planning, etc. Their usage in critical applications implies a more skeptical regard on their implementation, especially when the result is that a constraint problem has no solution, i.e., unsatisfiability. In this paper, we propose an approach aiming to develop a correct-by-construction finite domain based – CP(FD) – solver. We developed this solver within the Coq proof tool and proved its correctness in Coq. It embeds the algorithm AC3 (and AC2001) and uses arc-consistency. The Coq extraction mechanism allows us to provide a finite domain based solver written in OCaml formally verified, the first one to our knowledge. This solver can be used directly or as a second shot solver to verify results coming from an untrusted solver. This result has recently been published in FM 2012]. In this paper, we present a summary of this result and extend it to deal with another local-consistency property, namely, bound-consistency.