Trends in Constraint Programming

This 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 Contents:
Introduction 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