Exploiting functional dependencies in declarative problem specifications

摘要

In this paper we tackle the issue of the automatic recognition of functional dependencies among guessed predicates in constraint problem specifications. Functional dependencies arise frequently in pure declarative specifications, because of the intermediate results that need to be computed in order to express some of the constraints, or due to precise modeling choices, e.g., to provide multiple viewpoints of the search space in order to increase constraint propagation. In either way, the recognition of dependencies greatly helps solvers, allowing them to avoid spending search on unfruitful branches, while maintaining the highest degree of declarativeness. By modeling constraint problem specifications as second-order formulae, we provide a characterization of functional dependencies in terms of semantic properties of first-order ones, and prove undecidability of the problem of their recognition. Despite such negative result, we advocate the (in many cases effective) possibility of using automated tools to mechanize this task. Additionally, we show how suitable search procedures can be automatically synthesized in order to exploit recognized dependencies. We present opl examples of various problems, taken from bio-informatics, planning and resource allocation, and show how in many cases opl greatly benefits from the addition of such search procedures. Moreover, we also give evidence that writing sophisticated ad-hoc search procedures that handle dependencies exploiting the peculiarities of the particular problem is a very difficult and error-prone task which in many cases does not seem to pay-off.