Constraint modelling: A challenge for automated reasoning

Abstract

Cadoli et al [BCM04,MC05,CM04] noted the potential of first order automated reasoning for the purpose of analysing constraint models, and reported some encouraging initial experimental results. We are currently pursuing a very similar research program with a view to incorporating deductive technology in a state of the art constraint programming platform. Here we outline our own view of this application direction and discuss new empirical findings on a more extensive range of problems than those considered in the previous literature. While the opportunities presented by reasoning about constraint models are indeed exciting, we also find that there are formidable obstacles in the way of a practically useful implementation.