Frédéric Benhamou is a Full Professor in the Department of Computer Science and is Head of the Computer Science Research Laboratory at Nantes Atlantic University, France.  Narendra Jussien is the President of the French Association for Constraint Programming (AFPC) and is an Assistant Professor in the Department of Computer Science at the Ecole des Mines de Nantes, France. Barry O’Sullivan is the Associate Director of the Cork Constraint Computation Centre and is a Senior Lecturer in the Department of Computer Science at University College Cork, Ireland.

• Introduction 17Frédéric Benhamou, Narendra Jussien, Barry O’SullivanPart I. The Past, Present and Future of Constraint Programming 23Frédéric Benhamou, Narendra Jussien , Barry O’SullivanChapter 1. Constraint Programming as Declarative Algorithmics 25Pascal Van Hentenryck1.1. The CHIP project 261.2. The Numerica project 321.3. The OPL project 341.4. The Comet project 351.5. The future of constraint programming 38Chapter 2. Constraint Programming Tools 41Laurent Michel, Christian Schulte, Pascal Van Hentenryck2.1. Introduction 412.2. Invited talks 432.2.1. The development of an industrial CP tool (Jean-François Puget) 432.2.2. System design: taking informed decisions (Christian Schulte) 452.3. System presentations 482.3.1. ECLiPSe 482.3.2. SICStus FD 482.3.3. G12 492.3.4. DiSolver 492.3.5. MINION 502.3.6. Choco 502.3.7. Gecode 512.3.8. Comet 522.3.9. JaCoP 532.3.10. Borderwijk 542.4. Panels 542.5. Conclusion 562.6. References 57Chapter 3. The Next 10 Years of Constraint Programming 59Lucas Bordeaux, Barry O’Sullivan, Pascal Van Hentenryck3.1. Pedro Barahona 613.2. Christian Bessiere 633.3. Peter Jeavons 643.4. Pedro Meseguer 663.5. Gilles Pesant 683.6. Francesca Rossi 703.7. Thomas Schiex 723.8. Christian Schulte 743.9. Meinolf Sellmann 753.10. Mark Wallace 773.11. Toby Walsh 793.12. Roland Yap 803.13. References 81Chapter 4. Constraint Propagation and Implementation 83Marc van Dongen, Christophe Lecoutre4.1. Filtering algorithms for precedence and dependency constraints (by Roman Barták and Ondøej Èepek) 844.1.1. Problem description and related works 844.1.2. Filtering rules for precedence and dependency constraints 854.1.3. Summary 874.2. A study of residual supports in arc consistency (by Christophe Lecoutre and Fred Hemery) 874.3. Maintaining singleton arc consistency (by Christophe Lecoutre and Patrick Prosser) 894.3.1. Mixed consistency 904.3.2. Checking existential-SAC 914.3.3. Conclusion 924.4. Probabilistic singleton arc consistency (by Deepak Mehta and Marc van Dongen) 934.5. Simplification and extension of the SPREAD constraint (by Pierre Schaus, Yves Deville, Pierre Dupont and Jean-Charles Régin) 954.5.1. Filtering of π 964.5.2. Filtering of X 974.5.3. Conclusion 994.6. A new filtering algorithm for the graph isomorphism problem (by Sébastien Sorlin and Christine Solnon) 994.6.1. A global constraint for the graph isomorphism problem 994.6.2. ILL-consistency and ILL-filtering 1004.6.3. Experimental results 1024.7. References 103Chapter 5. On the First SAT/CP Integration Workshop 105Youssef Hamadi, Lucas Bordeaux5.1. The technical program 1065.1.1. The invited talk 1065.1.2. Contributions related to SMT and solver integration 1065.1.3. Contributions related to the use of SAT techniques to improve CSP/CP solvers 1075.1.4. Other contributions 1085.2. The panel session 1095.2.1. Are SAT and CP different or similar? 1095.2.2. Why has SAT succeeded in reducing the tuning issue? 1115.2.3. How long can the current generation of SAT solvers evolve? 1135.2.4. Were performance issues correctly addressed by CP? 1155.2.5. Was CP too ambitious? 1185.2.6. Do we still need CP? 1195.3. Summary, future directions and conclusion 1215.4. References 122Chapter 6. Constraint-Based Methods for Bioinformatics 125Alessandro Dal Palù, Agostino Dovier, Franæois Fages, Sebastian Will6.1. On using temporal logic with constraints to express biological properties of cell processes (by François Fages) 1266.2. Modeling biological systems in stochastic concurrent constraint programming (by Luca Bortolussi and Alberto Policriti) 1296.3. Chemera: constraints in protein structural problems (by Pedro Barahona and Ludwig Krippahl) 1326.4. Exploiting model checking in constraint-based approaches to the protein folding problem (by Elisabetta De Maria, Agostino Dovier, Angelo Montanari and Carla Piazza) 1346.5. Global constraints for discrete lattices (by Alessandro Dal Palù, Agostino Dovier and Enrico Pontelli) 1366.6. Counting protein structures by DFS with dynamic decomposition (by Sebastian Will and Martin Mann) 1386.7. Suffix array and weighted CSPs (by Matthias Zytnicki, Christine Gaspin and Thomas Schiex) 1416.8. Supertree construction with constraint programming: recent progress and new challenges (by Patrick Prosser) 1436.9. References 145Part II. Constraint Modeling and Reformulation 147Ian Miguel, Steven PrestwichChapter 7. Improved Models for Graceful Graphs 151Jean-François Puget, Barbara Smith7.1. Introduction 1517.2. A direct model 1527.3. The edge-label model 1547.4. A combined model 1567.5. Experimental results 1577.6. Discussion 1607.7. References 161Chapter 8. The Automatic Generation of Redundant Representations and Channeling Constraints 163Bernadette Martínez-Hernández, Alan M. Frisch8.1. Introduction 1638.2. Representations 1678.3. Alternative representations and channels 1688.3.1. Alternative representations 1688.3.2. Constraint-wise quasi-representations and channeling constraints 1698.4. Refinement 1748.5. Systematic generation of channeling constraints 1778.6. Producing the best alternative for channeling 1798.7. Conclusions and future work 1808.8. References 180Part III. Symmetry in Constraint Satisfaction Problems 183Alastair Donaldson, Peter Gregory, Karen PetrieChapter 9. GAPLex: Generalized Static Symmetry Breaking 187Chris Jefferson, Tom Kelsey, Steve Linton, Karen Petrie9.1. Background and introduction 1889.1.1. Group theory for CSPs 1909.1.2. Using GAP to break CSP symmetries 1919.2. GAPLex 1929.2.1. Motivation and rationale 1929.2.2. Motivating example 1939.2.3. The GAPLex algorithms 1939.3. Empirical evaluation 1969.3.1. Combining GAPLex with incomplete static SB methods 1979.3.2. Combining GAPLex with Puget’s all-different constraints 1989.4. Conclusions and future work 1999.5. References 199Chapter 10. Symmetry Breaking in Subgraph Pattern Matching 203Stéphane Zampelli, Yves Deville, Pierre Dupont10.1. Background and definitions 20510.2. Variable symmetries 20710.2.1. Detection 20710.2.2. Breaking 20710.3. Value symmetries 20810.3.1. Detection 20810.3.2. Breaking 20810.4. Experimental results 20910.5. Local value symmetries 21110.5.1. Dynamic target graph 21210.5.2. Partial dynamic graphs 21410.6. Conclusion 21510.7. References 216Part IV. Interval Analysis, Constraint Propagation and Applications 219Christophe Jermann, Yahia Lebbah, Djamila Sam-HaroudChapter 11. Modeling and Solving of a Radio Antenna Deployment Sup-port Application 223Michael Heusch11.1. Two simple models for the application 22411.1.1. A first finite domain model 22411.1.2. Shifting the model to mixed domains 22511.1.3. Description of the search algorithm 22511.1.4. Analysis of the performance on progressive deployment problems 22611.2. Introducing the distn constraint 22711.3. Modeling the application with the distn constraint 22811.3.1. Revised model of the application 22811.3.2. Numerical results when solving the LocRLFAP with distn 23011.3.3. Qualitative analysis of the results 23111.4. Conclusion 23111.5. References 232Chapter 12. Guaranteed Numerical Injectivity Test via Interval Analysis 233Sébastien Lagrange, Nicolas Delanoue, Luc Jaulin12.1. Interval analysis 23512.2. Injectivity 23612.2.1. Partial injectivity 23612.2.2. Partial injectivity condition 23812.3. ITVIA algorithm 24112.4. Examples 24212.4.1. Spiral function 24312.4.2. Ribbon function 24312.5. Conclusion 24412.6. References 244Chapter 13. An Interval-based Approximation Method for Discrete Changes in Hybrid cc 245Daisuke Ishii, Kazunori Ueda, Hiroshi Hosobe13.1. An overview of Hybrid cc 24613.1.1. The Hybrid cc language 24613.1.2. Implementation of Hybrid cc 24713.2. The objective of the chapter 24813.3. Background of interval arithmetic 24813.3.1. Basic notions of interval arithmetic 24913.3.2. ODE solving based on interval arithmetic 24913.4. The proposed method 24913.4.1. Assumptions on the proposed method 24913.4.2. Trace algorithm 25013.4.3. PruneAndMerge algorithm 25113.5. Experimental results 25213.6. Related work 25313.7. Conclusion 25413.8. References 254Part V. Local Search Techniques in Constraint Satisfaction 257Andrea Roli, Yehuda NavehChapter 14. Combining Adaptive Noise and Look-Ahead in Local Search for SAT 261Chu Min Li, Wanxia Wei, Harry Zhang14.1. Implementation of the adaptive noise mechanism in G2WSAT 26214.2. Look-Ahead for promising decreasing variables 26214.2.1. Promising score of a variable 26214.2.2. Integrating limited look-ahead in adaptG2WSAT 26314.3. Evaluation 26414.4. Conclusion 26614.5. References 266Chapter 15. Finding Large Cliques using SAT Local Search 269Steven Prestwich15.1. SAT-encoding the clique problem 27015.2. Notes on the bitwise at-most-one encoding 27115.3. Experiments 27215.4. Conclusion 27315.5. References 274Chapter 16. Multi-Point Constructive Search for Constraint Satisfac-tion: An Overview 275Ivan Heckman, J. Christopher Beck16.1. Background 27616.2. Empirical study 27716.3. Conclusion 27916.4. References 280Chapter 17. Boosting SLS Using Resolution 283Anbulagan, Duc Nghia Pham, John Slaney, Abdul Sattar17.1. SLS solvers 28417.2. Preprocessors 28517.3. Empirical evaluation 28617.3.1. Clause weighting versus random walk 28617.3.2. Matching preprocessors to solver-problem pairs 28717.3.3. Multiple preprocessing and preprocessor ordering 28717.4. Conclusion 28817.5. References 288Chapter 18. Growing COMET 291Pascal Van Hentenryck, Laurent Michel18.1. Constraint-based local search 29118.2. COMET 29218.3. Modeling 29318.4. Search 29518.5. References 296Part VI. Preferences and Soft Constraints 299Thomas SchiexChapter 19. The Logic Behind Weighted CSP 303Carlos Ansótegui, María L. Bonet, Jordi Levy, Felip Manyà19.1. Preliminaries 30419.2. The inference rule – soundness and completeness 30719.3. Global consistency in WCSP 31019.4. Local consistency in WCSP 31119.5. Conclusions 31419.6. References 316Chapter 20. Dynamic Heuristics for Branch and Bound on Tree-Decomposition of Weighted CSPs 317Philippe Jégou, Samba Ndojh Ndiaye, Cyril Terrioux20.1. Introduction 31720.2. Preliminaries 31920.3. Dynamic orders in O(exp(w + 1)) 32220.4. Bounded extensions of dynamic orders 32420.5. Heuristics 32520.5.1. Cluster orders 32520.5.2. Variable orders 32720.5.3. Heuristics for grouping variables in Classes 4 and 5 32720.6. Experimental study 32820.7. Discussion and conclusion 33020.8. References 331Part VII. Constraints in Software Testing, Verification and Analysis 333Benjamin Blanc, Arnaud Gotlieb, Claude MichelChapter 21. Extending a CP Solver with Congruences as Domains for Program Verification 337Michel Leconte, Bruno Berstel21.1. Related work 33921.2. Congruences as domains 33921.3. Propagation of congruences as domains 34021.4. Cooperation of congruences and intervals 34221.5. Conclusion 34221.6. References 343Chapter 22. Generating Random Values Using Binary Decision Dia-grams and Convex Polyhedra 345Erwan Jahier, Pascal Raymond22.1. BDD and convex polyhedra 34622.2. The resolution algorithm 34622.3. Choosing solutions 34822.4. Available tools 34922.5. Related work 35022.6. Conclusion 35122.7. References 351Chapter 23. A Symbolic Model for Hash-Collision Attacks 353Yannick Chevalier, Mounira Kourjieh23.1. Terms and subterms 35423.2. Analysis of reachability properties of cryptographic protocols 35623.3. Model of a collision-aware intruder 35723.3.1. Intruder on words 35723.3.2. Intruder on words with free function symbols 35823.3.3. Hash-colliding intruder 35823.4. Conclusion 35923.5. References 359Chapter 24. Strategy for Flaw Detection Based on a Service-driven Model for Group Protocols 361Najah Chridi, Laurent Vigneron24.1. Protocol modeling and attack search 36224.1.1. Input of the method 36224.1.2. Searching for attacks in group protocols 36324.1.3. Intruder knowledge management 36524.1.4. Constraint management 36624.2. Verification results 36624.3. Summary and future work 36724.4. References 368Part VIII. Constraint Programming for Graphical Applications 369Marc Christie, Hiroshi Hosobe and Kim MarriottChapter 25. Trends and Issues in using Constraint Programming for Graphical Applications 371Marc Christie, Hiroshi Hosobe and Kim Marriott25.1. More powerful constraint-solving techniques 37325.1.1. Mixture of discrete and continuous constraints 37325.1.2. Mixture of linear, polynomial, geometric and non-linear constraints 37325.1.3. Managing user interaction 37425.1.4. Managing preferences 37425.1.5. Generic techniques 37525.2. Better modeling and understanding of constraint systems by the end-user 37625.2.1. Model specification 37625.2.2. Extensibility 37725.2.3. Constraint representation 37725.2.4. Understanding constraint interaction during solving 37725.3. Bridging the gap between the solver and the application semantics 37825.3.1. High-level modeling 37925.3.2. Support for interaction 37925.4. Conclusion 37925.5. References 380Chapter 26. A Constraint Satisfaction Framework for Visual Problem Solving 383Bonny Banerjee, Balakrishnan Chandrasekaran26.1. The framework 38426.1.1. A language for expressing visual problems 38426.1.2. A visual problem solver 38826.2. Applications 39026.3. Conclusion 39326.4. References 393Chapter 27. Computer Graphics and Constraint Solving: An Applica-tion to Virtual Camera Control 395Jean-Marie Normand27.1. Overview 39727.2. A semantic space partitioning approach 39827.2.1. Projection property 39827.2.2. Orientation property 39927.2.3. Occlusion property 39927.3. Numerical solving stage 40027.4. Exploitation of semantic volumes 40127.4.1. Making requests on the volumes 40127.4.2. Making requests on the scene 40127.5. Results 40127.6. Discussion 40327.7. References 404Index 405

Frédéric Benhamou is a Full Professor in the Department of Computer Science and is Head of the Computer Science Research Laboratory at Nantes Atlantic University, France.  Narendra Jussien is the President of the French Association for Constraint Programming (AFPC) and is an Assistant Professor in the Department of Computer Science at the Ecole des Mines de Nantes, France. Barry O’Sullivan is the Associate Director of the Cork Constraint Computation Centre and is a Senior Lecturer in the Department of Computer Science at University College Cork, Ireland.

• Introduction 17Frédéric Benhamou, Narendra Jussien, Barry O’SullivanPart I. The Past, Present and Future of Constraint Programming 23Frédéric Benhamou, Narendra Jussien , Barry O’SullivanChapter 1. Constraint Programming as Declarative Algorithmics 25Pascal Van Hentenryck1.1. The CHIP project 261.2. The Numerica project 321.3. The OPL project 341.4. The Comet project 351.5. The future of constraint programming 38Chapter 2. Constraint Programming Tools 41Laurent Michel, Christian Schulte, Pascal Van Hentenryck2.1. Introduction 412.2. Invited talks 432.2.1. The development of an industrial CP tool (Jean-François Puget) 432.2.2. System design: taking informed decisions (Christian Schulte) 452.3. System presentations 482.3.1. ECLiPSe 482.3.2. SICStus FD 482.3.3. G12 492.3.4. DiSolver 492.3.5. MINION 502.3.6. Choco 502.3.7. Gecode 512.3.8. Comet 522.3.9. JaCoP 532.3.10. Borderwijk 542.4. Panels 542.5. Conclusion 562.6. References 57Chapter 3. The Next 10 Years of Constraint Programming 59Lucas Bordeaux, Barry O’Sullivan, Pascal Van Hentenryck3.1. Pedro Barahona 613.2. Christian Bessiere 633.3. Peter Jeavons 643.4. Pedro Meseguer 663.5. Gilles Pesant 683.6. Francesca Rossi 703.7. Thomas Schiex 723.8. Christian Schulte 743.9. Meinolf Sellmann 753.10. Mark Wallace 773.11. Toby Walsh 793.12. Roland Yap 803.13. References 81Chapter 4. Constraint Propagation and Implementation 83Marc van Dongen, Christophe Lecoutre4.1. Filtering algorithms for precedence and dependency constraints (by Roman Barták and Ondøej Èepek) 844.1.1. Problem description and related works 844.1.2. Filtering rules for precedence and dependency constraints 854.1.3. Summary 874.2. A study of residual supports in arc consistency (by Christophe Lecoutre and Fred Hemery) 874.3. Maintaining singleton arc consistency (by Christophe Lecoutre and Patrick Prosser) 894.3.1. Mixed consistency 904.3.2. Checking existential-SAC 914.3.3. Conclusion 924.4. Probabilistic singleton arc consistency (by Deepak Mehta and Marc van Dongen) 934.5. Simplification and extension of the SPREAD constraint (by Pierre Schaus, Yves Deville, Pierre Dupont and Jean-Charles Régin) 954.5.1. Filtering of π 964.5.2. Filtering of X 974.5.3. Conclusion 994.6. A new filtering algorithm for the graph isomorphism problem (by Sébastien Sorlin and Christine Solnon) 994.6.1. A global constraint for the graph isomorphism problem 994.6.2. ILL-consistency and ILL-filtering 1004.6.3. Experimental results 1024.7. References 103Chapter 5. On the First SAT/CP Integration Workshop 105Youssef Hamadi, Lucas Bordeaux5.1. The technical program 1065.1.1. The invited talk 1065.1.2. Contributions related to SMT and solver integration 1065.1.3. Contributions related to the use of SAT techniques to improve CSP/CP solvers 1075.1.4. Other contributions 1085.2. The panel session 1095.2.1. Are SAT and CP different or similar? 1095.2.2. Why has SAT succeeded in reducing the tuning issue? 1115.2.3. How long can the current generation of SAT solvers evolve? 1135.2.4. Were performance issues correctly addressed by CP? 1155.2.5. Was CP too ambitious? 1185.2.6. Do we still need CP? 1195.3. Summary, future directions and conclusion 1215.4. References 122Chapter 6. Constraint-Based Methods for Bioinformatics 125Alessandro Dal Palù, Agostino Dovier, Franæois Fages, Sebastian Will6.1. On using temporal logic with constraints to express biological properties of cell processes (by François Fages) 1266.2. Modeling biological systems in stochastic concurrent constraint programming (by Luca Bortolussi and Alberto Policriti) 1296.3. Chemera: constraints in protein structural problems (by Pedro Barahona and Ludwig Krippahl) 1326.4. Exploiting model checking in constraint-based approaches to the protein folding problem (by Elisabetta De Maria, Agostino Dovier, Angelo Montanari and Carla Piazza) 1346.5. Global constraints for discrete lattices (by Alessandro Dal Palù, Agostino Dovier and Enrico Pontelli) 1366.6. Counting protein structures by DFS with dynamic decomposition (by Sebastian Will and Martin Mann) 1386.7. Suffix array and weighted CSPs (by Matthias Zytnicki, Christine Gaspin and Thomas Schiex) 1416.8. Supertree construction with constraint programming: recent progress and new challenges (by Patrick Prosser) 1436.9. References 145Part II. Constraint Modeling and Reformulation 147Ian Miguel, Steven PrestwichChapter 7. Improved Models for Graceful Graphs 151Jean-François Puget, Barbara Smith7.1. Introduction 1517.2. A direct model 1527.3. The edge-label model 1547.4. A combined model 1567.5. Experimental results 1577.6. Discussion 1607.7. References 161Chapter 8. The Automatic Generation of Redundant Representations and Channeling Constraints 163Bernadette Martínez-Hernández, Alan M. Frisch8.1. Introduction 1638.2. Representations 1678.3. Alternative representations and channels 1688.3.1. Alternative representations 1688.3.2. Constraint-wise quasi-representations and channeling constraints 1698.4. Refinement 1748.5. Systematic generation of channeling constraints 1778.6. Producing the best alternative for channeling 1798.7. Conclusions and future work 1808.8. References 180Part III. Symmetry in Constraint Satisfaction Problems 183Alastair Donaldson, Peter Gregory, Karen PetrieChapter 9. GAPLex: Generalized Static Symmetry Breaking 187Chris Jefferson, Tom Kelsey, Steve Linton, Karen Petrie9.1. Background and introduction 1889.1.1. Group theory for CSPs 1909.1.2. Using GAP to break CSP symmetries 1919.2. GAPLex 1929.2.1. Motivation and rationale 1929.2.2. Motivating example 1939.2.3. The GAPLex algorithms 1939.3. Empirical evaluation 1969.3.1. Combining GAPLex with incomplete static SB methods 1979.3.2. Combining GAPLex with Puget’s all-different constraints 1989.4. Conclusions and future work 1999.5. References 199Chapter 10. Symmetry Breaking in Subgraph Pattern Matching 203Stéphane Zampelli, Yves Deville, Pierre Dupont10.1. Background and definitions 20510.2. Variable symmetries 20710.2.1. Detection 20710.2.2. Breaking 20710.3. Value symmetries 20810.3.1. Detection 20810.3.2. Breaking 20810.4. Experimental results 20910.5. Local value symmetries 21110.5.1. Dynamic target graph 21210.5.2. Partial dynamic graphs 21410.6. Conclusion 21510.7. References 216Part IV. Interval Analysis, Constraint Propagation and Applications 219Christophe Jermann, Yahia Lebbah, Djamila Sam-HaroudChapter 11. Modeling and Solving of a Radio Antenna Deployment Sup-port Application 223Michael Heusch11.1. Two simple models for the application 22411.1.1. A first finite domain model 22411.1.2. Shifting the model to mixed domains 22511.1.3. Description of the search algorithm 22511.1.4. Analysis of the performance on progressive deployment problems 22611.2. Introducing the distn constraint 22711.3. Modeling the application with the distn constraint 22811.3.1. Revised model of the application 22811.3.2. Numerical results when solving the LocRLFAP with distn 23011.3.3. Qualitative analysis of the results 23111.4. Conclusion 23111.5. References 232Chapter 12. Guaranteed Numerical Injectivity Test via Interval Analysis 233Sébastien Lagrange, Nicolas Delanoue, Luc Jaulin12.1. Interval analysis 23512.2. Injectivity 23612.2.1. Partial injectivity 23612.2.2. Partial injectivity condition 23812.3. ITVIA algorithm 24112.4. Examples 24212.4.1. Spiral function 24312.4.2. Ribbon function 24312.5. Conclusion 24412.6. References 244Chapter 13. An Interval-based Approximation Method for Discrete Changes in Hybrid cc 245Daisuke Ishii, Kazunori Ueda, Hiroshi Hosobe13.1. An overview of Hybrid cc 24613.1.1. The Hybrid cc language 24613.1.2. Implementation of Hybrid cc 24713.2. The objective of the chapter 24813.3. Background of interval arithmetic 24813.3.1. Basic notions of interval arithmetic 24913.3.2. ODE solving based on interval arithmetic 24913.4. The proposed method 24913.4.1. Assumptions on the proposed method 24913.4.2. Trace algorithm 25013.4.3. PruneAndMerge algorithm 25113.5. Experimental results 25213.6. Related work 25313.7. Conclusion 25413.8. References 254Part V. Local Search Techniques in Constraint Satisfaction 257Andrea Roli, Yehuda NavehChapter 14. Combining Adaptive Noise and Look-Ahead in Local Search for SAT 261Chu Min Li, Wanxia Wei, Harry Zhang14.1. Implementation of the adaptive noise mechanism in G2WSAT 26214.2. Look-Ahead for promising decreasing variables 26214.2.1. Promising score of a variable 26214.2.2. Integrating limited look-ahead in adaptG2WSAT 26314.3. Evaluation 26414.4. Conclusion 26614.5. References 266Chapter 15. Finding Large Cliques using SAT Local Search 269Steven Prestwich15.1. SAT-encoding the clique problem 27015.2. Notes on the bitwise at-most-one encoding 27115.3. Experiments 27215.4. Conclusion 27315.5. References 274Chapter 16. Multi-Point Constructive Search for Constraint Satisfac-tion: An Overview 275Ivan Heckman, J. Christopher Beck16.1. Background 27616.2. Empirical study 27716.3. Conclusion 27916.4. References 280Chapter 17. Boosting SLS Using Resolution 283Anbulagan, Duc Nghia Pham, John Slaney, Abdul Sattar17.1. SLS solvers 28417.2. Preprocessors 28517.3. Empirical evaluation 28617.3.1. Clause weighting versus random walk 28617.3.2. Matching preprocessors to solver-problem pairs 28717.3.3. Multiple preprocessing and preprocessor ordering 28717.4. Conclusion 28817.5. References 288Chapter 18. Growing COMET 291Pascal Van Hentenryck, Laurent Michel18.1. Constraint-based local search 29118.2. COMET 29218.3. Modeling 29318.4. Search 29518.5. References 296Part VI. Preferences and Soft Constraints 299Thomas SchiexChapter 19. The Logic Behind Weighted CSP 303Carlos Ansótegui, María L. Bonet, Jordi Levy, Felip Manyà19.1. Preliminaries 30419.2. The inference rule – soundness and completeness 30719.3. Global consistency in WCSP 31019.4. Local consistency in WCSP 31119.5. Conclusions 31419.6. References 316Chapter 20. Dynamic Heuristics for Branch and Bound on Tree-Decomposition of Weighted CSPs 317Philippe Jégou, Samba Ndojh Ndiaye, Cyril Terrioux20.1. Introduction 31720.2. Preliminaries 31920.3. Dynamic orders in O(exp(w + 1)) 32220.4. Bounded extensions of dynamic orders 32420.5. Heuristics 32520.5.1. Cluster orders 32520.5.2. Variable orders 32720.5.3. Heuristics for grouping variables in Classes 4 and 5 32720.6. Experimental study 32820.7. Discussion and conclusion 33020.8. References 331Part VII. Constraints in Software Testing, Verification and Analysis 333Benjamin Blanc, Arnaud Gotlieb, Claude MichelChapter 21. Extending a CP Solver with Congruences as Domains for Program Verification 337Michel Leconte, Bruno Berstel21.1. Related work 33921.2. Congruences as domains 33921.3. Propagation of congruences as domains 34021.4. Cooperation of congruences and intervals 34221.5. Conclusion 34221.6. References 343Chapter 22. Generating Random Values Using Binary Decision Dia-grams and Convex Polyhedra 345Erwan Jahier, Pascal Raymond22.1. BDD and convex polyhedra 34622.2. The resolution algorithm 34622.3. Choosing solutions 34822.4. Available tools 34922.5. Related work 35022.6. Conclusion 35122.7. References 351Chapter 23. A Symbolic Model for Hash-Collision Attacks 353Yannick Chevalier, Mounira Kourjieh23.1. Terms and subterms 35423.2. Analysis of reachability properties of cryptographic protocols 35623.3. Model of a collision-aware intruder 35723.3.1. Intruder on words 35723.3.2. Intruder on words with free function symbols 35823.3.3. Hash-colliding intruder 35823.4. Conclusion 35923.5. References 359Chapter 24. Strategy for Flaw Detection Based on a Service-driven Model for Group Protocols 361Najah Chridi, Laurent Vigneron24.1. Protocol modeling and attack search 36224.1.1. Input of the method 36224.1.2. Searching for attacks in group protocols 36324.1.3. Intruder knowledge management 36524.1.4. Constraint management 36624.2. Verification results 36624.3. Summary and future work 36724.4. References 368Part VIII. Constraint Programming for Graphical Applications 369Marc Christie, Hiroshi Hosobe and Kim MarriottChapter 25. Trends and Issues in using Constraint Programming for Graphical Applications 371Marc Christie, Hiroshi Hosobe and Kim Marriott25.1. More powerful constraint-solving techniques 37325.1.1. Mixture of discrete and continuous constraints 37325.1.2. Mixture of linear, polynomial, geometric and non-linear constraints 37325.1.3. Managing user interaction 37425.1.4. Managing preferences 37425.1.5. Generic techniques 37525.2. Better modeling and understanding of constraint systems by the end-user 37625.2.1. Model specification 37625.2.2. Extensibility 37725.2.3. Constraint representation 37725.2.4. Understanding constraint interaction during solving 37725.3. Bridging the gap between the solver and the application semantics 37825.3.1. High-level modeling 37925.3.2. Support for interaction 37925.4. Conclusion 37925.5. References 380Chapter 26. A Constraint Satisfaction Framework for Visual Problem Solving 383Bonny Banerjee, Balakrishnan Chandrasekaran26.1. The framework 38426.1.1. A language for expressing visual problems 38426.1.2. A visual problem solver 38826.2. Applications 39026.3. Conclusion 39326.4. References 393Chapter 27. Computer Graphics and Constraint Solving: An Applica-tion to Virtual Camera Control 395Jean-Marie Normand27.1. Overview 39727.2. A semantic space partitioning approach 39827.2.1. Projection property 39827.2.2. Orientation property 39927.2.3. Occlusion property 39927.3. Numerical solving stage 40027.4. Exploitation of semantic volumes 40127.4.1. Making requests on the volumes 40127.4.2. Making requests on the scene 40127.5. Results 40127.6. Discussion 40327.7. References 404Index 405

Frédéric Benhamou is a Full Professor in the Department of Computer Science and is Head of the Computer Science Research Laboratory at Nantes Atlantic University, France.  Narendra Jussien is the President of the French Association for Constraint Programming (AFPC) and is an Assistant Professor in the Department of Computer Science at the Ecole des Mines de Nantes, France. Barry O’Sullivan is the Associate Director of the Cork Constraint Computation Centre and is a Senior Lecturer in the Department of Computer Science at University College Cork, Ireland.

• Introduction 17Frédéric Benhamou, Narendra Jussien, Barry O’SullivanPart I. The Past, Present and Future of Constraint Programming 23Frédéric Benhamou, Narendra Jussien , Barry O’SullivanChapter 1. Constraint Programming as Declarative Algorithmics 25Pascal Van Hentenryck1.1. The CHIP project 261.2. The Numerica project 321.3. The OPL project 341.4. The Comet project 351.5. The future of constraint programming 38Chapter 2. Constraint Programming Tools 41Laurent Michel, Christian Schulte, Pascal Van Hentenryck2.1. Introduction 412.2. Invited talks 432.2.1. The development of an industrial CP tool (Jean-François Puget) 432.2.2. System design: taking informed decisions (Christian Schulte) 452.3. System presentations 482.3.1. ECLiPSe 482.3.2. SICStus FD 482.3.3. G12 492.3.4. DiSolver 492.3.5. MINION 502.3.6. Choco 502.3.7. Gecode 512.3.8. Comet 522.3.9. JaCoP 532.3.10. Borderwijk 542.4. Panels 542.5. Conclusion 562.6. References 57Chapter 3. The Next 10 Years of Constraint Programming 59Lucas Bordeaux, Barry O’Sullivan, Pascal Van Hentenryck3.1. Pedro Barahona 613.2. Christian Bessiere 633.3. Peter Jeavons 643.4. Pedro Meseguer 663.5. Gilles Pesant 683.6. Francesca Rossi 703.7. Thomas Schiex 723.8. Christian Schulte 743.9. Meinolf Sellmann 753.10. Mark Wallace 773.11. Toby Walsh 793.12. Roland Yap 803.13. References 81Chapter 4. Constraint Propagation and Implementation 83Marc van Dongen, Christophe Lecoutre4.1. Filtering algorithms for precedence and dependency constraints (by Roman Barták and Ondøej Èepek) 844.1.1. Problem description and related works 844.1.2. Filtering rules for precedence and dependency constraints 854.1.3. Summary 874.2. A study of residual supports in arc consistency (by Christophe Lecoutre and Fred Hemery) 874.3. Maintaining singleton arc consistency (by Christophe Lecoutre and Patrick Prosser) 894.3.1. Mixed consistency 904.3.2. Checking existential-SAC 914.3.3. Conclusion 924.4. Probabilistic singleton arc consistency (by Deepak Mehta and Marc van Dongen) 934.5. Simplification and extension of the SPREAD constraint (by Pierre Schaus, Yves Deville, Pierre Dupont and Jean-Charles Régin) 954.5.1. Filtering of π 964.5.2. Filtering of X 974.5.3. Conclusion 994.6. A new filtering algorithm for the graph isomorphism problem (by Sébastien Sorlin and Christine Solnon) 994.6.1. A global constraint for the graph isomorphism problem 994.6.2. ILL-consistency and ILL-filtering 1004.6.3. Experimental results 1024.7. References 103Chapter 5. On the First SAT/CP Integration Workshop 105Youssef Hamadi, Lucas Bordeaux5.1. The technical program 1065.1.1. The invited talk 1065.1.2. Contributions related to SMT and solver integration 1065.1.3. Contributions related to the use of SAT techniques to improve CSP/CP solvers 1075.1.4. Other contributions 1085.2. The panel session 1095.2.1. Are SAT and CP different or similar? 1095.2.2. Why has SAT succeeded in reducing the tuning issue? 1115.2.3. How long can the current generation of SAT solvers evolve? 1135.2.4. Were performance issues correctly addressed by CP? 1155.2.5. Was CP too ambitious? 1185.2.6. Do we still need CP? 1195.3. Summary, future directions and conclusion 1215.4. References 122Chapter 6. Constraint-Based Methods for Bioinformatics 125Alessandro Dal Palù, Agostino Dovier, Franæois Fages, Sebastian Will6.1. On using temporal logic with constraints to express biological properties of cell processes (by François Fages) 1266.2. Modeling biological systems in stochastic concurrent constraint programming (by Luca Bortolussi and Alberto Policriti) 1296.3. Chemera: constraints in protein structural problems (by Pedro Barahona and Ludwig Krippahl) 1326.4. Exploiting model checking in constraint-based approaches to the protein folding problem (by Elisabetta De Maria, Agostino Dovier, Angelo Montanari and Carla Piazza) 1346.5. Global constraints for discrete lattices (by Alessandro Dal Palù, Agostino Dovier and Enrico Pontelli) 1366.6. Counting protein structures by DFS with dynamic decomposition (by Sebastian Will and Martin Mann) 1386.7. Suffix array and weighted CSPs (by Matthias Zytnicki, Christine Gaspin and Thomas Schiex) 1416.8. Supertree construction with constraint programming: recent progress and new challenges (by Patrick Prosser) 1436.9. References 145Part II. Constraint Modeling and Reformulation 147Ian Miguel, Steven PrestwichChapter 7. Improved Models for Graceful Graphs 151Jean-François Puget, Barbara Smith7.1. Introduction 1517.2. A direct model 1527.3. The edge-label model 1547.4. A combined model 1567.5. Experimental results 1577.6. Discussion 1607.7. References 161Chapter 8. The Automatic Generation of Redundant Representations and Channeling Constraints 163Bernadette Martínez-Hernández, Alan M. Frisch8.1. Introduction 1638.2. Representations 1678.3. Alternative representations and channels 1688.3.1. Alternative representations 1688.3.2. Constraint-wise quasi-representations and channeling constraints 1698.4. Refinement 1748.5. Systematic generation of channeling constraints 1778.6. Producing the best alternative for channeling 1798.7. Conclusions and future work 1808.8. References 180Part III. Symmetry in Constraint Satisfaction Problems 183Alastair Donaldson, Peter Gregory, Karen PetrieChapter 9. GAPLex: Generalized Static Symmetry Breaking 187Chris Jefferson, Tom Kelsey, Steve Linton, Karen Petrie9.1. Background and introduction 1889.1.1. Group theory for CSPs 1909.1.2. Using GAP to break CSP symmetries 1919.2. GAPLex 1929.2.1. Motivation and rationale 1929.2.2. Motivating example 1939.2.3. The GAPLex algorithms 1939.3. Empirical evaluation 1969.3.1. Combining GAPLex with incomplete static SB methods 1979.3.2. Combining GAPLex with Puget’s all-different constraints 1989.4. Conclusions and future work 1999.5. References 199Chapter 10. Symmetry Breaking in Subgraph Pattern Matching 203Stéphane Zampelli, Yves Deville, Pierre Dupont10.1. Background and definitions 20510.2. Variable symmetries 20710.2.1. Detection 20710.2.2. Breaking 20710.3. Value symmetries 20810.3.1. Detection 20810.3.2. Breaking 20810.4. Experimental results 20910.5. Local value symmetries 21110.5.1. Dynamic target graph 21210.5.2. Partial dynamic graphs 21410.6. Conclusion 21510.7. References 216Part IV. Interval Analysis, Constraint Propagation and Applications 219Christophe Jermann, Yahia Lebbah, Djamila Sam-HaroudChapter 11. Modeling and Solving of a Radio Antenna Deployment Sup-port Application 223Michael Heusch11.1. Two simple models for the application 22411.1.1. A first finite domain model 22411.1.2. Shifting the model to mixed domains 22511.1.3. Description of the search algorithm 22511.1.4. Analysis of the performance on progressive deployment problems 22611.2. Introducing the distn constraint 22711.3. Modeling the application with the distn constraint 22811.3.1. Revised model of the application 22811.3.2. Numerical results when solving the LocRLFAP with distn 23011.3.3. Qualitative analysis of the results 23111.4. Conclusion 23111.5. References 232Chapter 12. Guaranteed Numerical Injectivity Test via Interval Analysis 233Sébastien Lagrange, Nicolas Delanoue, Luc Jaulin12.1. Interval analysis 23512.2. Injectivity 23612.2.1. Partial injectivity 23612.2.2. Partial injectivity condition 23812.3. ITVIA algorithm 24112.4. Examples 24212.4.1. Spiral function 24312.4.2. Ribbon function 24312.5. Conclusion 24412.6. References 244Chapter 13. An Interval-based Approximation Method for Discrete Changes in Hybrid cc 245Daisuke Ishii, Kazunori Ueda, Hiroshi Hosobe13.1. An overview of Hybrid cc 24613.1.1. The Hybrid cc language 24613.1.2. Implementation of Hybrid cc 24713.2. The objective of the chapter 24813.3. Background of interval arithmetic 24813.3.1. Basic notions of interval arithmetic 24913.3.2. ODE solving based on interval arithmetic 24913.4. The proposed method 24913.4.1. Assumptions on the proposed method 24913.4.2. Trace algorithm 25013.4.3. PruneAndMerge algorithm 25113.5. Experimental results 25213.6. Related work 25313.7. Conclusion 25413.8. References 254Part V. Local Search Techniques in Constraint Satisfaction 257Andrea Roli, Yehuda NavehChapter 14. Combining Adaptive Noise and Look-Ahead in Local Search for SAT 261Chu Min Li, Wanxia Wei, Harry Zhang14.1. Implementation of the adaptive noise mechanism in G2WSAT 26214.2. Look-Ahead for promising decreasing variables 26214.2.1. Promising score of a variable 26214.2.2. Integrating limited look-ahead in adaptG2WSAT 26314.3. Evaluation 26414.4. Conclusion 26614.5. References 266Chapter 15. Finding Large Cliques using SAT Local Search 269Steven Prestwich15.1. SAT-encoding the clique problem 27015.2. Notes on the bitwise at-most-one encoding 27115.3. Experiments 27215.4. Conclusion 27315.5. References 274Chapter 16. Multi-Point Constructive Search for Constraint Satisfac-tion: An Overview 275Ivan Heckman, J. Christopher Beck16.1. Background 27616.2. Empirical study 27716.3. Conclusion 27916.4. References 280Chapter 17. Boosting SLS Using Resolution 283Anbulagan, Duc Nghia Pham, John Slaney, Abdul Sattar17.1. SLS solvers 28417.2. Preprocessors 28517.3. Empirical evaluation 28617.3.1. Clause weighting versus random walk 28617.3.2. Matching preprocessors to solver-problem pairs 28717.3.3. Multiple preprocessing and preprocessor ordering 28717.4. Conclusion 28817.5. References 288Chapter 18. Growing COMET 291Pascal Van Hentenryck, Laurent Michel18.1. Constraint-based local search 29118.2. COMET 29218.3. Modeling 29318.4. Search 29518.5. References 296Part VI. Preferences and Soft Constraints 299Thomas SchiexChapter 19. The Logic Behind Weighted CSP 303Carlos Ansótegui, María L. Bonet, Jordi Levy, Felip Manyà19.1. Preliminaries 30419.2. The inference rule – soundness and completeness 30719.3. Global consistency in WCSP 31019.4. Local consistency in WCSP 31119.5. Conclusions 31419.6. References 316Chapter 20. Dynamic Heuristics for Branch and Bound on Tree-Decomposition of Weighted CSPs 317Philippe Jégou, Samba Ndojh Ndiaye, Cyril Terrioux20.1. Introduction 31720.2. Preliminaries 31920.3. Dynamic orders in O(exp(w + 1)) 32220.4. Bounded extensions of dynamic orders 32420.5. Heuristics 32520.5.1. Cluster orders 32520.5.2. Variable orders 32720.5.3. Heuristics for grouping variables in Classes 4 and 5 32720.6. Experimental study 32820.7. Discussion and conclusion 33020.8. References 331Part VII. Constraints in Software Testing, Verification and Analysis 333Benjamin Blanc, Arnaud Gotlieb, Claude MichelChapter 21. Extending a CP Solver with Congruences as Domains for Program Verification 337Michel Leconte, Bruno Berstel21.1. Related work 33921.2. Congruences as domains 33921.3. Propagation of congruences as domains 34021.4. Cooperation of congruences and intervals 34221.5. Conclusion 34221.6. References 343Chapter 22. Generating Random Values Using Binary Decision Dia-grams and Convex Polyhedra 345Erwan Jahier, Pascal Raymond22.1. BDD and convex polyhedra 34622.2. The resolution algorithm 34622.3. Choosing solutions 34822.4. Available tools 34922.5. Related work 35022.6. Conclusion 35122.7. References 351Chapter 23. A Symbolic Model for Hash-Collision Attacks 353Yannick Chevalier, Mounira Kourjieh23.1. Terms and subterms 35423.2. Analysis of reachability properties of cryptographic protocols 35623.3. Model of a collision-aware intruder 35723.3.1. Intruder on words 35723.3.2. Intruder on words with free function symbols 35823.3.3. Hash-colliding intruder 35823.4. Conclusion 35923.5. References 359Chapter 24. Strategy for Flaw Detection Based on a Service-driven Model for Group Protocols 361Najah Chridi, Laurent Vigneron24.1. Protocol modeling and attack search 36224.1.1. Input of the method 36224.1.2. Searching for attacks in group protocols 36324.1.3. Intruder knowledge management 36524.1.4. Constraint management 36624.2. Verification results 36624.3. Summary and future work 36724.4. References 368Part VIII. Constraint Programming for Graphical Applications 369Marc Christie, Hiroshi Hosobe and Kim MarriottChapter 25. Trends and Issues in using Constraint Programming for Graphical Applications 371Marc Christie, Hiroshi Hosobe and Kim Marriott25.1. More powerful constraint-solving techniques 37325.1.1. Mixture of discrete and continuous constraints 37325.1.2. Mixture of linear, polynomial, geometric and non-linear constraints 37325.1.3. Managing user interaction 37425.1.4. Managing preferences 37425.1.5. Generic techniques 37525.2. Better modeling and understanding of constraint systems by the end-user 37625.2.1. Model specification 37625.2.2. Extensibility 37725.2.3. Constraint representation 37725.2.4. Understanding constraint interaction during solving 37725.3. Bridging the gap between the solver and the application semantics 37825.3.1. High-level modeling 37925.3.2. Support for interaction 37925.4. Conclusion 37925.5. References 380Chapter 26. A Constraint Satisfaction Framework for Visual Problem Solving 383Bonny Banerjee, Balakrishnan Chandrasekaran26.1. The framework 38426.1.1. A language for expressing visual problems 38426.1.2. A visual problem solver 38826.2. Applications 39026.3. Conclusion 39326.4. References 393Chapter 27. Computer Graphics and Constraint Solving: An Applica-tion to Virtual Camera Control 395Jean-Marie Normand27.1. Overview 39727.2. A semantic space partitioning approach 39827.2.1. Projection property 39827.2.2. Orientation property 39927.2.3. Occlusion property 39927.3. Numerical solving stage 40027.4. Exploitation of semantic volumes 40127.4.1. Making requests on the volumes 40127.4.2. Making requests on the scene 40127.5. Results 40127.6. Discussion 40327.7. References 404Index 405