Search

Literature on Constraint Satisfaction exhibits the definition of several "structural" properties that can be possessed by CSPs, like (in)consistency, substitutability or interchangeability. Current tools for constraint solving typically detect such properties efficiently by means of incomplete yet effective algorithms, and use them to reduce the search space and boost search. In this paper, we provide a unifying framework encompassing most of the properties known so far, both in CSP and other fields' literature, and shed light on the semantical relationships among them. This gives a unified and comprehensive view of the topic, allows new, unknown, properties to emerge, and clarifies the computational complexity of the various detection problems. In particular, among the others, two new concepts, fixability and removability emerge, that come out to be the ideal characterisations of values that may be safely assigned or removed from a variable's domain, while preserving problem satisfiability. These two notions subsume a large number of known properties, including inconsistency, substitutability and others. Because of the computational intractability of all the property-detection problems, by following the CSP approach we then determine a number of relaxations which provide sufficient conditions for their tractability. In particular, we exploit forms of language restrictions and local reasoning. [ABSTRACT FROM AUTHOR]

Abstract: 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. [Copyright &y& Elsevier]

The efficiency of systems for constraint programming (CP) is currently highly affected by the actual formulation of the input problem. To this end, several choices have to be made by modelers in order to write efficient specifications and handle instances of realistic size, and this, of course, represents a major obstacle to reach full declarativeness. Several structural properties of problem specifications have been investigated in order to provide techniques that reformulate a constraint program into one which is more efficiently evaluable by the solver at hand. In this paper we consider two such properties, symmetries and functional dependencies among variables, and show that, by characterizing problem specifications as logical formulae, the task of deciding whether such properties hold, and consequently that of performing the relevant reformulations, can be practically mechanized by means of automated theorem proving (ATP) technology. In particular, we report the results on using ATP technology for checking the existence of symmetries, checking whether a given constraint is symmetry-breaking, and checking the existence of functional dependencies in a specification. The output of the reasoning phase is a transformed constraint program, consisting in a reformulated specification and, possibly, a search strategy. We show our techniques on problems such as graph coloring, Sailco inventory, and protein folding. [ABSTRACT FROM AUTHOR]

Abstract: In this paper we propose a form of reasoning on specifications of combinatorial problems, with the goal of reformulating them so that they are more efficiently solvable. The reformulation technique highlights constraints that can be safely “delayed”, and solved afterwards. Our main contribution is the characterization (with soundness proof) of safe-delay constraints with respect to a criterion on the specification, thus obtaining a mechanism for the automated reformulation of specifications applicable to a great variety of problems, e.g., graph coloring, bin-packing, and job-shop scheduling. This is an advancement with respect to the forms of reasoning done by state-of-the-art-systems, which typically just detect linearity of specifications. Another contribution is an experimentation on the effectiveness of the proposed technique using six different solvers, which reveals promising time savings. [Copyright &y& Elsevier]