Description
Book SynopsisThis title brings together the best papers on a range of topics raised at the annual International Conference on Principles and Practice of Constraint Programming. This conference provides papers and workshops which produce new insights, concepts and results which can then be used by those involved in this area to develop their own work.
Table of ContentsIntroduction 17
Frédéric Benhamou, Narendra Jussien, Barry O’Sullivan
Part I. The Past, Present and Future of Constraint Programming 23
Frédéric Benhamou, Narendra Jussien , Barry O’Sullivan
Chapter 1. Constraint Programming as Declarative Algorithmics 25
Pascal Van Hentenryck
1.1. The CHIP project 26
1.2. The Numerica project 32
1.3. The OPL project 34
1.4. The Comet project 35
1.5. The future of constraint programming 38
Chapter 2. Constraint Programming Tools 41
Laurent Michel, Christian Schulte, Pascal Van Hentenryck
2.1. Introduction 41
2.2. Invited talks 43
2.2.1. The development of an industrial CP tool (Jean-François Puget) 43
2.2.2. System design: taking informed decisions (Christian Schulte) 45
2.3. System presentations 48
2.3.1. ECLiPSe 48
2.3.2. SICStus FD 48
2.3.3. G12 49
2.3.4. DiSolver 49
2.3.5. MINION 50
2.3.6. Choco 50
2.3.7. Gecode 51
2.3.8. Comet 52
2.3.9. JaCoP 53
2.3.10. Borderwijk 54
2.4. Panels 54
2.5. Conclusion 56
2.6. References 57
Chapter 3. The Next 10 Years of Constraint Programming 59
Lucas Bordeaux, Barry O’Sullivan, Pascal Van Hentenryck
3.1. Pedro Barahona 61
3.2. Christian Bessiere 63
3.3. Peter Jeavons 64
3.4. Pedro Meseguer 66
3.5. Gilles Pesant 68
3.6. Francesca Rossi 70
3.7. Thomas Schiex 72
3.8. Christian Schulte 74
3.9. Meinolf Sellmann 75
3.10. Mark Wallace 77
3.11. Toby Walsh 79
3.12. Roland Yap 80
3.13. References 81
Chapter 4. Constraint Propagation and Implementation 83
Marc van Dongen, Christophe Lecoutre
4.1. Filtering algorithms for precedence and dependency constraints (by Roman Barták and Ondøej Èepek) 84
4.1.1. Problem description and related works 84
4.1.2. Filtering rules for precedence and dependency constraints 85
4.1.3. Summary 87
4.2. A study of residual supports in arc consistency (by Christophe Lecoutre and Fred Hemery) 87
4.3. Maintaining singleton arc consistency (by Christophe Lecoutre and Patrick Prosser) 89
4.3.1. Mixed consistency 90
4.3.2. Checking existential-SAC 91
4.3.3. Conclusion 92
4.4. Probabilistic singleton arc consistency (by Deepak Mehta and Marc van Dongen) 93
4.5. Simplification and extension of the SPREAD constraint (by Pierre Schaus, Yves Deville, Pierre Dupont and Jean-Charles Régin) 95
4.5.1. Filtering of π 96
4.5.2. Filtering of X 97
4.5.3. Conclusion 99
4.6. A new filtering algorithm for the graph isomorphism problem (by Sébastien Sorlin and Christine Solnon) 99
4.6.1. A global constraint for the graph isomorphism problem 99
4.6.2. ILL-consistency and ILL-filtering 100
4.6.3. Experimental results 102
4.7. References 103
Chapter 5. On the First SAT/CP Integration Workshop 105
Youssef Hamadi, Lucas Bordeaux
5.1. The technical program 106
5.1.1. The invited talk 106
5.1.2. Contributions related to SMT and solver integration 106
5.1.3. Contributions related to the use of SAT techniques to improve CSP/CP solvers 107
5.1.4. Other contributions 108
5.2. The panel session 109
5.2.1. Are SAT and CP different or similar? 109
5.2.2. Why has SAT succeeded in reducing the tuning issue? 111
5.2.3. How long can the current generation of SAT solvers evolve? 113
5.2.4. Were performance issues correctly addressed by CP? 115
5.2.5. Was CP too ambitious? 118
5.2.6. Do we still need CP? 119
5.3. Summary, future directions and conclusion 121
5.4. References 122
Chapter 6. Constraint-Based Methods for Bioinformatics 125
Alessandro Dal Palù, Agostino Dovier, Franæois Fages, Sebastian Will
6.1. On using temporal logic with constraints to express biological properties of cell processes (by François Fages) 126
6.2. Modeling biological systems in stochastic concurrent constraint programming (by Luca Bortolussi and Alberto Policriti) 129
6.3. Chemera: constraints in protein structural problems (by Pedro Barahona and Ludwig Krippahl) 132
6.4. Exploiting model checking in constraint-based approaches to the protein folding problem (by Elisabetta De Maria, Agostino Dovier, Angelo Montanari and Carla Piazza) 134
6.5. Global constraints for discrete lattices (by Alessandro Dal Palù, Agostino Dovier and Enrico Pontelli) 136
6.6. Counting protein structures by DFS with dynamic decomposition (by Sebastian Will and Martin Mann) 138
6.7. Suffix array and weighted CSPs (by Matthias Zytnicki, Christine Gaspin and Thomas Schiex) 141
6.8. Supertree construction with constraint programming: recent progress and new challenges (by Patrick Prosser) 143
6.9. References 145
Part II. Constraint Modeling and Reformulation 147
Ian Miguel, Steven Prestwich
Chapter 7. Improved Models for Graceful Graphs 151
Jean-François Puget, Barbara Smith
7.1. Introduction 151
7.2. A direct model 152
7.3. The edge-label model 154
7.4. A combined model 156
7.5. Experimental results 157
7.6. Discussion 160
7.7. References 161
Chapter 8. The Automatic Generation of Redundant Representations and Channeling Constraints 163
Bernadette Martínez-Hernández, Alan M. Frisch
8.1. Introduction 163
8.2. Representations 167
8.3. Alternative representations and channels 168
8.3.1. Alternative representations 168
8.3.2. Constraint-wise quasi-representations and channeling constraints 169
8.4. Refinement 174
8.5. Systematic generation of channeling constraints 177
8.6. Producing the best alternative for channeling 179
8.7. Conclusions and future work 180
8.8. References 180
Part III. Symmetry in Constraint Satisfaction Problems 183
Alastair Donaldson, Peter Gregory, Karen Petrie
Chapter 9. GAPLex: Generalized Static Symmetry Breaking 187
Chris Jefferson, Tom Kelsey, Steve Linton, Karen Petrie
9.1. Background and introduction 188
9.1.1. Group theory for CSPs 190
9.1.2. Using GAP to break CSP symmetries 191
9.2. GAPLex 192
9.2.1. Motivation and rationale 192
9.2.2. Motivating example 193
9.2.3. The GAPLex algorithms 193
9.3. Empirical evaluation 196
9.3.1. Combining GAPLex with incomplete static SB methods 197
9.3.2. Combining GAPLex with Puget’s all-different constraints 198
9.4. Conclusions and future work 199
9.5. References 199
Chapter 10. Symmetry Breaking in Subgraph Pattern Matching 203
Stéphane Zampelli, Yves Deville, Pierre Dupont
10.1. Background and definitions 205
10.2. Variable symmetries 207
10.2.1. Detection 207
10.2.2. Breaking 207
10.3. Value symmetries 208
10.3.1. Detection 208
10.3.2. Breaking 208
10.4. Experimental results 209
10.5. Local value symmetries 211
10.5.1. Dynamic target graph 212
10.5.2. Partial dynamic graphs 214
10.6. Conclusion 215
10.7. References 216
Part IV. Interval Analysis, Constraint Propagation and Applications 219
Christophe Jermann, Yahia Lebbah, Djamila Sam-Haroud
Chapter 11. Modeling and Solving of a Radio Antenna Deployment Sup-port Application 223
Michael Heusch
11.1. Two simple models for the application 224
11.1.1. A first finite domain model 224
11.1.2. Shifting the model to mixed domains 225
11.1.3. Description of the search algorithm 225
11.1.4. Analysis of the performance on progressive deployment problems 226
11.2. Introducing the distn constraint 227
11.3. Modeling the application with the distn constraint 228
11.3.1. Revised model of the application 228
11.3.2. Numerical results when solving the LocRLFAP with distn 230
11.3.3. Qualitative analysis of the results 231
11.4. Conclusion 231
11.5. References 232
Chapter 12. Guaranteed Numerical Injectivity Test via Interval Analysis 233
Sébastien Lagrange, Nicolas Delanoue, Luc Jaulin
12.1. Interval analysis 235
12.2. Injectivity 236
12.2.1. Partial injectivity 236
12.2.2. Partial injectivity condition 238
12.3. ITVIA algorithm 241
12.4. Examples 242
12.4.1. Spiral function 243
12.4.2. Ribbon function 243
12.5. Conclusion 244
12.6. References 244
Chapter 13. An Interval-based Approximation Method for Discrete Changes in Hybrid cc 245
Daisuke Ishii, Kazunori Ueda, Hiroshi Hosobe
13.1. An overview of Hybrid cc 246
13.1.1. The Hybrid cc language 246
13.1.2. Implementation of Hybrid cc 247
13.2. The objective of the chapter 248
13.3. Background of interval arithmetic 248
13.3.1. Basic notions of interval arithmetic 249
13.3.2. ODE solving based on interval arithmetic 249
13.4. The proposed method 249
13.4.1. Assumptions on the proposed method 249
13.4.2. Trace algorithm 250
13.4.3. PruneAndMerge algorithm 251
13.5. Experimental results 252
13.6. Related work 253
13.7. Conclusion 254
13.8. References 254
Part V. Local Search Techniques in Constraint Satisfaction 257
Andrea Roli, Yehuda Naveh
Chapter 14. Combining Adaptive Noise and Look-Ahead in Local Search for SAT 261
Chu Min Li, Wanxia Wei, Harry Zhang
14.1. Implementation of the adaptive noise mechanism in G2WSAT 262
14.2. Look-Ahead for promising decreasing variables 262
14.2.1. Promising score of a variable 262
14.2.2. Integrating limited look-ahead in adaptG2WSAT 263
14.3. Evaluation 264
14.4. Conclusion 266
14.5. References 266
Chapter 15. Finding Large Cliques using SAT Local Search 269
Steven Prestwich
15.1. SAT-encoding the clique problem 270
15.2. Notes on the bitwise at-most-one encoding 271
15.3. Experiments 272
15.4. Conclusion 273
15.5. References 274
Chapter 16. Multi-Point Constructive Search for Constraint Satisfac-tion: An Overview 275
Ivan Heckman, J. Christopher Beck
16.1. Background 276
16.2. Empirical study 277
16.3. Conclusion 279
16.4. References 280
Chapter 17. Boosting SLS Using Resolution 283
Anbulagan, Duc Nghia Pham, John Slaney, Abdul Sattar
17.1. SLS solvers 284
17.2. Preprocessors 285
17.3. Empirical evaluation 286
17.3.1. Clause weighting versus random walk 286
17.3.2. Matching preprocessors to solver-problem pairs 287
17.3.3. Multiple preprocessing and preprocessor ordering 287
17.4. Conclusion 288
17.5. References 288
Chapter 18. Growing COMET 291
Pascal Van Hentenryck, Laurent Michel
18.1. Constraint-based local search 291
18.2. COMET 292
18.3. Modeling 293
18.4. Search 295
18.5. References 296
Part VI. Preferences and Soft Constraints 299
Thomas Schiex
Chapter 19. The Logic Behind Weighted CSP 303
Carlos Ansótegui, María L. Bonet, Jordi Levy, Felip Manyà
19.1. Preliminaries 304
19.2. The inference rule – soundness and completeness 307
19.3. Global consistency in WCSP 310
19.4. Local consistency in WCSP 311
19.5. Conclusions 314
19.6. References 316
Chapter 20. Dynamic Heuristics for Branch and Bound on Tree-Decomposition of Weighted CSPs 317
Philippe Jégou, Samba Ndojh Ndiaye, Cyril Terrioux
20.1. Introduction 317
20.2. Preliminaries 319
20.3. Dynamic orders in O(exp(w + 1)) 322
20.4. Bounded extensions of dynamic orders 324
20.5. Heuristics 325
20.5.1. Cluster orders 325
20.5.2. Variable orders 327
20.5.3. Heuristics for grouping variables in Classes 4 and 5 327
20.6. Experimental study 328
20.7. Discussion and conclusion 330
20.8. References 331
Part VII. Constraints in Software Testing, Verification and Analysis 333
Benjamin Blanc, Arnaud Gotlieb, Claude Michel
Chapter 21. Extending a CP Solver with Congruences as Domains for Program Verification 337
Michel Leconte, Bruno Berstel
21.1. Related work 339
21.2. Congruences as domains 339
21.3. Propagation of congruences as domains 340
21.4. Cooperation of congruences and intervals 342
21.5. Conclusion 342
21.6. References 343
Chapter 22. Generating Random Values Using Binary Decision Dia-grams and Convex Polyhedra 345
Erwan Jahier, Pascal Raymond
22.1. BDD and convex polyhedra 346
22.2. The resolution algorithm 346
22.3. Choosing solutions 348
22.4. Available tools 349
22.5. Related work 350
22.6. Conclusion 351
22.7. References 351
Chapter 23. A Symbolic Model for Hash-Collision Attacks 353
Yannick Chevalier, Mounira Kourjieh
23.1. Terms and subterms 354
23.2. Analysis of reachability properties of cryptographic protocols 356
23.3. Model of a collision-aware intruder 357
23.3.1. Intruder on words 357
23.3.2. Intruder on words with free function symbols 358
23.3.3. Hash-colliding intruder 358
23.4. Conclusion 359
23.5. References 359
Chapter 24. Strategy for Flaw Detection Based on a Service-driven Model for Group Protocols 361
Najah Chridi, Laurent Vigneron
24.1. Protocol modeling and attack search 362
24.1.1. Input of the method 362
24.1.2. Searching for attacks in group protocols 363
24.1.3. Intruder knowledge management 365
24.1.4. Constraint management 366
24.2. Verification results 366
24.3. Summary and future work 367
24.4. References 368
Part VIII. Constraint Programming for Graphical Applications 369
Marc Christie, Hiroshi Hosobe and Kim Marriott
Chapter 25. Trends and Issues in using Constraint Programming for Graphical Applications 371
Marc Christie, Hiroshi Hosobe and Kim Marriott
25.1. More powerful constraint-solving techniques 373
25.1.1. Mixture of discrete and continuous constraints 373
25.1.2. Mixture of linear, polynomial, geometric and non-linear constraints 373
25.1.3. Managing user interaction 374
25.1.4. Managing preferences 374
25.1.5. Generic techniques 375
25.2. Better modeling and understanding of constraint systems by the end-user 376
25.2.1. Model specification 376
25.2.2. Extensibility 377
25.2.3. Constraint representation 377
25.2.4. Understanding constraint interaction during solving 377
25.3. Bridging the gap between the solver and the application semantics 378
25.3.1. High-level modeling 379
25.3.2. Support for interaction 379
25.4. Conclusion 379
25.5. References 380
Chapter 26. A Constraint Satisfaction Framework for Visual Problem Solving 383
Bonny Banerjee, Balakrishnan Chandrasekaran
26.1. The framework 384
26.1.1. A language for expressing visual problems 384
26.1.2. A visual problem solver 388
26.2. Applications 390
26.3. Conclusion 393
26.4. References 393
Chapter 27. Computer Graphics and Constraint Solving: An Applica-tion to Virtual Camera Control 395
Jean-Marie Normand
27.1. Overview 397
27.2. A semantic space partitioning approach 398
27.2.1. Projection property 398
27.2.2. Orientation property 399
27.2.3. Occlusion property 399
27.3. Numerical solving stage 400
27.4. Exploitation of semantic volumes 401
27.4.1. Making requests on the volumes 401
27.4.2. Making requests on the scene 401
27.5. Results 401
27.6. Discussion 403
27.7. References 404
Index 405
