Catálogo de publicaciones - libros

The typical constraint store transmits a limited amount of information because it consists only of variable domains. We propose a richer constraint store in the form of a limited-width multivalued decision diagram (MDD). It reduces to a traditional domain store when the maximum width is one but allows greater pruning of the search tree for larger widths. MDD propagation algorithms can be developed to exploit the structure of particular constraints, much as is done for domain filtering algorithms. We propose specialized propagation algorithms for alldiff and inequality constraints. Preliminary experiments show that MDD propagation solves multiple alldiff problems an order of magnitude more rapidly than traditional domain propagation. It also significantly reduces the search tree for inequality problems, but additional research is needed to reduce the computation time.

In this paper we argue that an attractive and potentially very general way of achieving generalized arc consistency (GAC) on a constraint is by using unit propagation (UP) over a CNF encoding of the constraint. This approach to GAC offers a number of advantages over traditional constraint specific algorithms (propagators): it is easier to implement, it automatically provides incrementality and decrementality in a backtracking context, and it can provide clausal reasons to support learning and non-chronological backtracking. Although UP on standard CNF encodings of a constraint fails to achieve GAC, we show here that alternate CNF encodings can be used on which UP does achieve GAC. We provide a generic encoding applicable to any constraint. We also give structure specific encodings for the , , and constraints on which UP can achieve GAC with the same run time bounds as previously presented propagators. Finally, we explain how a UP engine can be added to a CSP solver to achieve a seamless integration of constraints encoded in CNF and propagated via UP and those propagated via traditional constraint specific propagators.

In this paper we present new techniques for improving backtracking based Quantified Constraint Satisfaction Problem (QCSP) solvers. QCSP is a generalization of CSP in which variables are either universally or existentially quantified and these quantifiers can be alternated in arbitrary ways. Our main new technique is solution directed backjumping (SBJ). In analogue to conflict directed backjumping, SBJ allows the solver to backtrack out of solved sub-trees without having to find all of the distinct solutions normally required to validate the universal variables. Experiments with the solver QCSP-Solve demonstrate that SBJ can improve its performance on random instances by orders of magnitude. In addition to this contribution, we demonstrate that performing varying levels of propagation for universal vs. existential variables can also be useful for enhancing performance. Finally, we discuss some techniques that are technically interesting but do not yet yield empirical improvements.

While many real-world combinatorial problems can be advantageously modeled and solved using Constraint Programming, scalability remains a major issue in practice. Constraint models that accurately reflect the inherent structure of a problem, solvers that exploit the properties of this structure, and reformulation techniques that modify the problem encoding to reduce the cost of problem solving are typically used to overcome the complexity barrier. In this paper, we investigate such approaches in a geospatial reasoning task, the building-identification problem (BID), introduced and modeled as a Constraint Satisfaction Problem by Michalowski and Knoblock [1]. We introduce an improved constraint model, a custom solver for this problem, and a number of reformulation techniques that modify various aspects of the problem encoding to improve scalability. We show how interleaving these reformulations with the various stages of the solver allows us to solve much larger BID problems than was previously possible. Importantly, we describe the usefulness of our reformulations techniques for general Constraint Satisfaction Problems, beyond the BID application.

This paper introduces a geometrical constraint kernel for handling the location in space and time of polymorphic -dimensional objects subject to various geometrical and time constraints. The constraint kernel is generic in the sense that one of its parameters is a set of constraints on subsets of the objects. These constraints are handled globally by the kernel.

We first illustrate how to model several placement problems with the constraint kernel. We then explain how new constraints can be introduced and plugged into the kernel. Based on these interfaces, we develop a generic -dimensional lexicographic sweep algorithm for filtering the attributes of an object (i.e., its shape and the coordinates of its origin as well as its start, duration and end in time) according to all constraints where the object occurs. Experiments involving up to hundreds of thousands of objects and 1 million integer variables are provided in 2, 3 and 4 dimensions, both for simple shapes (i.e., rectangles, parallelepipeds) and for more complex shapes.

Many research works on symmetry in CSPs appeared recently. But, most of them deal only with the global symmetry of the studied problem and give no strategy that can be used to detect and eliminate local symmetry. Eliminating global symmetry is shown to be useful, but exploiting only these symmetries could not be sufficient to solve some hard locally symmetrical problems. That is, a problem can have few or no initial symmetries and become very symmetrical at some nodes during the search. In this paper we study a general principle of semantic symmetry and define a syntactic symmetry which is a sufficient condition for semantic symmetry. We define a weakened form of this syntactic symmetry, and show how to detect and how to eliminate it locally to increase CSP tree search methods efficiency. Experiments confirm that local symmetry breaking is profitable for CSP solving.

The constraint is useful in modelling car sequencing, rostering, scheduling and related problems. We introduce half a dozen new encodings of the constraint, some of which do not hinder propagation. We prove that, down a branch of a search tree, domain consistency can be enforced on the constraint in just ( log) time. This improves upon the previous bound of () for each call down the tree. We also consider a generalization of the constraint – the Multiple constraint. Our experiments suggest that, on very large and tight problems, domain consistency algorithms are best. However, on smaller or looser problems, much simpler encodings are better, even though these encodings hinder propagation. When there are multiple constraints, a more expensive propagator shows promise.

Recent research has focused on using the power of look-ahead to speed up the resolution of the Max-SAT problem. Indeed, look-ahead techniques such as Unit Propagation (UP) allow to find conflicts and to quickly reach the upper bound in a Branch-and-Bound algorithm, reducing the search-space of the resolution. In previous works, the Max-SAT solvers 9 and 14 use unit propagation to compute, at each node of the branch and bound search-tree, disjoint inconsistent subsets of clauses in the current subformula to estimate the minimum number of clauses that cannot be satisfied by any assignment extended from the current node. The same subsets may still be present in the subtrees, that is why we present in this paper a new method to memorize them and then spare their recomputation time. Furthermore, we propose a heuristic so that the memorized subsets of clauses induce an ordering among unit clauses to detect more inconsistent subsets of clauses. We show that this new approach improves 9 and 14 and suggest that the approach can also be used to improve other state-of-the-art Max-SAT solvers.

We present the constraint combinator that models while loops in Constraint Programming. Embedded in a finite domain constraint solver, it allows programmers to develop non-trivial arithmetical relations using loops, exactly as in an imperative language style. The deduction capabilities of this combinator come from abstract interpretation over the polyhedra abstract domain. This combinator has already demonstrated its utility in constraint-based verification and we argue that it also facilitates the rapid prototyping of arithmetic constraints (e.g. power, gcd or sum).

There has been considerable interest in the identification of structural properties of combinatorial problems that lead to efficient algorithms for solving them. Some of these properties are “easily” identifiable, while others are of interest because they capture key aspects of state-of-the-art constraint solvers. In particular, it was recently shown that the problem of identifying a strong Horn- or 2CNF-backdoor can be solved by exploiting equivalence with deletion backdoors, and is NP-complete. We prove that strong backdoor identification becomes harder than NP (unless NP=coNP) as soon as the inconsequential sounding feature of empty clause detection (present in all modern SAT solvers) is added. More interestingly, in practice such a feature as well as polynomial time constraint propagation mechanisms often lead to much smaller backdoor sets. In fact, despite the worst-case complexity results for strong backdoor detection, we show that Satz-Rand is remarkably good at finding small strong backdoors on a range of experimental domains. Our results suggest that structural notions explored for designing efficient algorithms for combinatorial problems should capture both statically and dynamically identifiable properties.