Catálogo de publicaciones - libros

Compartir en
redes sociales


Principles and Practice of Constraint Programming: CP 2007: 13th International Conference, CP 2007, Providence, RI, USA, September 23-27, 2007. Proceedings

Christian Bessière (eds.)

En conferencia: 13º International Conference on Principles and Practice of Constraint Programming (CP) . Providence, RI, USA . September 23, 2007 - September 27, 2007

Resumen/Descripción – provisto por la editorial

No disponible.

Palabras clave – provistas por la editorial

No disponibles.

Disponibilidad
Institución detectada Año de publicación Navegá Descargá Solicitá
No detectada 2007 SpringerLink

Información

Tipo de recurso:

libros

ISBN impreso

978-3-540-74969-1

ISBN electrónico

978-3-540-74970-7

Editor responsable

Springer Nature

País de edición

Reino Unido

Fecha de publicación

Información sobre derechos de publicación

© Springer-Verlag Berlin Heidelberg 2007

Tabla de contenidos

Breaking Symmetry of Interchangeable Variables and Values

Y. C. Law; J. H. M. Lee; Toby Walsh; J. Y. K. Yip

A common type of symmetry is when both variables and values partition into interchangeable sets. Polynomial methods have been introduced to eliminate all symmetric solutions introduced by such interchangeability. Unfortunately, whilst eliminating all symmetric solutions is tractable in this case, pruning all symmetric values is NP-hard. We introduce a new global constraint called and its GAC propagator for pruning some (but not necessarily all) symmetric values. We also investigate how different postings of the constraints affect the pruning performance during constraint solving. Finally, we test these static symmetry breaking constraints experimentally for the first time.

- Full Research Papers | Pp. 423-437

Path Consistency by Dual Consistency

Christophe Lecoutre; Stéphane Cardon; Julien Vion

Dual Consistency (DC) is a property of Constraint Networks (CNs) which is equivalent, in its unrestricted form, to Path Consistency (PC). The principle is to perform successive singleton checks (i.e. enforcing arc consistency after the assignment of a value to a variable) in order to identify inconsistent pairs of values, until a fixpoint is reached. In this paper, we propose two new algorithms, denoted by sDC2 and sDC3, to enforce (strong) PC following the DC approach. These algorithms can be seen as refinements of Mac Gregor’s algorithm as they partially and totally exploit the incrementality of the underlying Arc Consistency algorithm. While sDC3 admits the same interesting worst-case complexities as PC8, sDC2 appears to be the most robust algorithm in practice. Indeed, compared to PC8 and the optimal PC2001, sDC2 is usually around one order of magnitude faster on large instances.

- Full Research Papers | Pp. 438-452

Exploiting Past and Future: Pruning by Inconsistent Partial State Dominance

Christophe Lecoutre; Lakhdar Sais; Sébastien Tabary; Vincent Vidal

It has recently been shown, for the Constraint Satisfaction Problem (CSP), that the state associated with a node of the search tree built by a backtracking algorithm can be exploited, using a transposition table, to prevent the exploration of similar nodes. This technique is commonly used in game search algorithms, heuristic search or planning. Its application is made possible in CSP by computing a partial state – a set of meaningful variables and their associated domains – preserving relevant information. We go further in this paper by providing two new powerful operators dedicated to the extraction of inconsistent partial states. The first one eliminates any variable whose current domain can be deduced from the partial state, and the second one extracts the variables involved in the inconsistency proof of the subtree rooted by the current node. Interestingly, we show these two operators can be safely combined, and that the pruning capabilities of the recorded partial states can be improved by a dominance detection approach (using lazy data structures).

- Full Research Papers | Pp. 453-467

Scheduling Conditional Task Graphs

Michele Lombardi; Michela Milano

This paper describes a complete and efficient solution to the scheduling of conditional task graphs whose nodes are activities and whose arcs can be labelled with a probability distribution. Tasks are executed if a set of conditions hold at scheduling execution time. The model is therefore stochastic. The minimization of the expected makespan implies an exponential-sized description of the objective function. We propose an analytic formulation of the stochastic objective function based on the task graph analysis, and a conditional constraint that handles it efficiently. Experimental results show the effectiveness of our approach in comparison with (1) an approach using a deterministic objective function and (2) scenario based constraint programming taking into account all scenarios or only a part of them.

- Full Research Papers | Pp. 468-482

Towards Robust CNF Encodings of Cardinality Constraints

Joao Marques-Silva; Inês Lynce

Motivated by the performance improvements made to SAT solvers in recent years, a number of different encodings of constraints into SAT have been proposed. Concrete examples are the different SAT encodings for ≤ 1 (,...,) constraints. The most widely used encoding is known as the pairwise encoding, which is quadratic in the number of variables in the constraint. Alternative encodings are in general linear, and require using additional auxiliary variables. In most settings, the pairwise encoding performs acceptably well, but can require unacceptably large Boolean formulas. In contrast, linear encodings yield much smaller Boolean formulas, but in practice SAT solvers often perform unpredictably. This lack of predictability is mostly due to the large number of auxiliary variables that need to be added to the resulting Boolean formula. This paper studies one specific encoding for ≤ 1 (,...,) constraints, and shows how a state-of-the-art SAT solver can be adapted to overcome the problem of adding additional auxiliary variables. Moreover, the paper shows that a SAT solver may essentially ignore the existence of auxiliary variables. Experimental results indicate that the modified SAT solver becomes significantly more robust on SAT encodings involving ≤ 1 (,...,) constraints.

- Full Research Papers | Pp. 483-497

AND/OR Multi-valued Decision Diagrams for Constraint Optimization

Robert Mateescu; Radu Marinescu; Rina Dechter

We propose a new top down search-based algorithm for compiling AND/OR Multi-Valued Decision Diagrams (AOMDDs), as representations of the optimal set of solutions for constraint optimization problems. The approach is based on AND/OR search spaces for graphical models, state-of-the-art AND/OR Branch-and-Bound search, and on decision diagrams reduction techniques. We extend earlier work on AOMDDs by considering general weighted graphs based on cost functions rather than constraints. An extensive experimental evaluation proves the efficiency of the weighted AOMDD data structure.

- Full Research Papers | Pp. 498-513

Parallelizing Constraint Programs Transparently

Laurent Michel; Andrew See; Pascal Van Hentenryck

The availability of commodity multi-core and multi-processor machines and the inherent parallelism in constraint programming search offer significant opportunities for constraint programming. They also present a fundamental challenge: how to exploit parallelism transparently to speed up constraint programs. This paper shows how to parallelize constraint programs transparently without changes to the code. The main technical idea consists of automatically lifting a sequential exploration strategy into its parallel counterpart, allowing workers to share and steal subproblems. Experimental results show that the parallel implementation may produces significant speedups on multi-core machines.

- Full Research Papers | Pp. 514-528

MiniZinc: Towards a Standard CP Modelling Language

Nicholas Nethercote; Peter J. Stuckey; Ralph Becket; Sebastian Brand; Gregory J. Duck; Guido Tack

There is no standard modelling language for constraint programming (CP) problems. Most solvers have their own modelling language. This makes it difficult for modellers to experiment with different solvers for a problem.

In this paper we present MiniZinc, a simple but expressive CP modelling language which is suitable for modelling problems for a range of solvers and provides a reasonable compromise between many design possibilities. Equally importantly, we also propose a low-level solver-input language called FlatZinc, and a straightforward translation from MiniZinc to FlatZinc that preserves all solver-supported global constraints. This lets a solver writer support MiniZinc with a minimum of effort—they only need to provide a simple FlatZinc front-end to their solver, and then combine it with an existing MiniZinc-to-FlatZinc translator. Such a front-end may then serve as a stepping stone towards a full MiniZinc implementation that is more tailored to the particular solver.

A standard language for modelling CP problems will encourage experimentation with and comparisons between different solvers. Although MiniZinc is not perfect—no standard modelling language will be—we believe its simplicity, expressiveness, and ease of implementation make it a practical choice for a standard language.

- Full Research Papers | Pp. 529-543

Propagation = Lazy Clause Generation

Olga Ohrimenko; Peter J. Stuckey; Michael Codish

Finite domain propagation solvers effectively represent the possible values of variables by a set of choices which can be naturally modelled as Boolean variables. In this paper we describe how we can mimic a finite domain propagation engine, by mapping propagators into clauses in a SAT solver. This immediately results in strong nogoods for finite domain propagation. But a naive static translation is impractical except in limited cases. We show how we can convert propagators to lazy clause generators for a SAT solver. The resulting system can solve scheduling problems significantly faster than generating the clauses from scratch, or using Satisfiability Modulo Theories solvers with difference logic.

- Full Research Papers | Pp. 544-558

Boosting Probabilistic Choice Operators

Matthieu Petit; Arnaud Gotlieb

Probabilistic Choice Operators (PCOs) are convenient tools to model uncertainty in CP. They are useful to implement randomized algorithms and stochastic processes in the concurrent constraint framework. Their implementation is based on the random selection of a value inside a finite domain according to a given probability distribution. Unfortunately, the probabilistic choice of a PCO is usually delayed until the probability distribution is completely known. This is inefficient and penalizes their broader adoption in real-world applications. In this paper, we associate to PCO a filtering algorithm that prunes the variation domain of its random variable during constraint propagation. Our algorithm runs in () where denotes the size of the domain of the probabilistic choice. Experimental results show the practical interest of this approach.

- Full Research Papers | Pp. 559-573