Arrays are ubiquitous in the context of software verication. However, eective reasoning over arrays is still rare in CP, as local reasoning is dramatically ill-conditioned for constraints over arrays. In this paper, we propose an approach com- bining both global symbolic reasoning and local consistency ltering in order to solve constraint systems involving arrays (with accesses, updates and size constraints) and nite-domain constraints over their elements and indexes. Our approach, named fdcc, is based on a combination of a congruence closure algorithm for the standard theory of arrays and a CP solver over nite domains. The tricky part of the work lies in the bi- directional communication mechanism between both solvers. We identify the signicant information to share, and design ways to master the communication overhead. Exper- iments on random instances show that fdcc solves more formulas than any portfolio combination of the two solvers taken in isolation, while overhead is kept reasonable.
Combination of propagators in CP. Several possibilities can be considered to implement constraint propagation when multiple propagators are available @cite_12 . First, an external solver can be embedded as a new global constraint in , as done for example on the Quad global constraint for continuous domains @cite_14 . This approach offers global reasoning over the constraint store. However, it requires fine control over the awakening mechanism of the new global constraint. A second approach consists in calling both solvers in a concurrent way. Each of them is launched on a distinct thread, and both threads prune a common constraint store that serves of blackboard. This approach has been successfully implemented in Oz @cite_18 . The difficulty is to identify which information must be shared, and to do it efficiently. A third approach consists in building a master-slave combination process where one of the solvers (here ) drives the computation and call the other ( ). The difficulty here is to understand when the master must call the slave. We follow mainly the second approach, however a third agent (the supervisor) acts as a lightweight master over and to synchronise both solvers through queries.
@cite_18 @cite_14 @cite_12
2035811095 1542480886 1626677565 1984594269
This article presents a model and implementation techniques for speeding up constraint propagation. Three fundamental approaches to improving constraint propagation based on propagators as implementations of constraints are explored: keeping track of which propagators are at fixpoint, choosing which propagator to apply next, and how to combine several propagators for the same constraint. We show how idempotence reasoning and events help track fixpoints more accurately. We improve these methods by using them dynamically (taking into account current variable domains to improve accuracy). We define priority-based approaches to choosing a next propagator and show that dynamic priorities can improve propagation. We illustrate that the use of multiple propagators for the same constraint can be advantageous with priorities, and introduce staged propagators that combine the effects of multiple propagators with priorities for greater efficiency. Constraint Programming (CP) has been successfully applied to several combinatorial optimization problems. One of its advantages is the availability of complex global constraints performing efficient propagation and interacting with each other through shared variables. However, CP techniques have shown their limitations in dealing with optimization problems since the link between the objective function and problem decision variables is often quite loose and does not produce an effective propagation. We propose to integrate optimization components in global constraints, aimed at optimally solving a relaxation corresponding to the constraint itself. The optimal solution of the relaxation provides pieces of information which can be exploited in order to perform pruning on the basis of cost-based reasoning. In fact, we exploit reduction rules based on lower bound and reduced costs calculation to remove those branches which cannot improve the best solution found so far. The interest of integrating efficient well-known Operations Research (OR) algorithms into CP is mainly due to the smooth interaction between CP domain reduction and information provided by the relaxation acting on variable domains which can be seen as a i>communication channel among different techniques. We have applied this technique to symmetric and asymmetric Traveling Salesman Problem (TSP) instances both because the TSP is an interesting problem arising in many real-life applications, and because pure CP techniques lead to disappointing results for this problem. We have tested the proposed optimization constraints using ILOG solver. Computational results on benchmarks available from literature, and comparison with related approaches are described in the paper. The proposed method on pure TSPs improves the performances of CP solvers, but is still far from the OR state of the art techniques for solving the problem. However, due to the flexibility of the CP framework, we could easily use the same technique on TSP with Time Windows, a time constrained variant of the TSP. For this type of problem, we achieve results that are comparable with state of the art OR results. We study propagation algorithms for the conjunction of two ALLDIFFERENT constraints. Solutions of an ALLDIFFERENT constraint can be seen as perfect matchings on the variable value bipartite graph. Therefore, we investigate the problem of finding simultaneous bipartite match-ings. We present an extension of the famous Hall theorem which characterizes when simultaneous bipartite matchings exists. Unfortunately, finding such matchings is NP-hard in general. However, we prove a surprising result that finding a simultaneous matching on a convex bipartite graph takes just polynomial time. Based on this theoretical result, we provide the first polynomial time bound consistency algorithm for the conjunction of two ALLDIFFERENT constraints. We identify a pathological problem on which this propagator is exponentially faster compared to existing propagators. Our experiments show that this new propagator can offer significant benefits over existing methods. A parallel version of a new hybrid genetic algorithm for the vehicle routing problem with time windows is presented. The route-directed hybrid genetic approach is based upon the simultaneous evolution of two populations of solutions focusing on separate objectives subject to temporal constraint relaxation. While the first population evolves individuals to minimize total traveled distance the second aims at minimizing temporal constraint violation to generate a feasible solution. Genetic operators have been designed to capture key concepts from successful routing techniques to further enhance search diversification and intensification. A master–slave message-passing paradigm characterizes the parallel procedure. The master component controls the execution of the algorithm, coordinates genetic operations and handles parent selection while the slave elements concurrently execute reproduction and mutation operators. Providing additional speed-up, the parallel algorithm further expands on its sequential counterpart, matching or even improving solution quality. Computational results show the proposed technique to be very competitive with the best-known heuristic routing procedures providing some new best-known solutions.