8:15 - 9:00 | Registration and Opening | |
9:00 - 10:15 |
John Chinneck
|
|
10:15 - 10:45 | Coffee Break | |
10:45 - 12:00 |
Gilles Pesant
|
|
12:00 - 13:30 | Lunch Break | |
13:30 - 14:45 |
Marijn Heule
|
|
14:45 - 15:15 | Coffee Break | |
15:15 - 16:30 |
Nathan Sturtevant
|
|
16:30 - 16:45 | Stretch Break | |
16:45 - 18:00 |
John Chinneck, Gilles Pesant, Marijn Heule, Nathan Sturtevant
Panel Session: Ideas for Crossfertilization and Hybrids
|
|
18:00 - later | Master Class Reception |
Lecture: Search in Mixed-Integer Linear Programming (slides for download)
Research on methods for solving Mixed-Integer Linear Programs (MIPs) dates to 1956. This long history means that MIP researchers proposed many of the seminal ideas in search that are echoed in other disciplines. At the same time, the Linear Programming (LP) structure inherent in MIP means that some search techniques are peculiar to MIP. The presentation is a tutorial overview of the main ideas relating to search in MIP, along with a summary of more recent ideas and techniques. The two most important topics are node selection and branching variable selection, and the principles motivating the choice of heuristics for each of these.Lecture: (Backtrack) Search in Constraint Programming (slides for download)
Constraint Programming originated for the most part from the field of Artificial Intelligence and is thus similarly structured around Representation and Search. The former led to declarative models and powerful inference algorithms encapsulated in each of their constraints. The latter offers programmable search that can be tailored to a specific problem, most often based on backtrack search. Much of the originality and success of Constraint Programming so far has come from the side of inference but there has been growing interest lately in robust generic search heuristics as key to the widespread use of this technology. The presentation is a tutorial overview of the main ideas relating to search in CP (search tree traversal, variable and value selection heuristics) along with a summary of more recent ideas and techniques (e.g. learning during search, impact-based search, counting-based search).Lecture: Search in SAT (slides for download)
Satisfiability (SAT) solvers have become powerful search engines to solve a wide range of applications in fields such as formal verification, planning and bio-informatics. Due to the elementary representation of SAT problems, many low-level optimizations can be implemented. At the same time, there exist clause-based techniques that can simulate several high-level reasoning methods. The tutorial focuses on the search procedures in successful conflict-driven clause learning SAT solvers. It shows how to learn from conflicts and provides an overview of effective heuristics for variable and value selection. Additionally, the presentation covers recent developments, in particular a technique used in today's strongest solvers: the alternation between "classic" depth-first search with learning, and breadth-first search for simplification.Lecture: The Deployment of Fast A* Search (slides for download)
Research in heuristic search over the last 25 years has often tended towards domains that grow exponentially, often typified by puzzles such as the sliding tile puzzle or Rubik's cube. But, in the last five years there have been a great number of advancements for search in domains that fit in memory where very fast search is required. This tutorial will begin with the basics of A* search with consistent and inconsistent heuristics, and then cover recent algorithms used for search in road networks and in games, with detailed examples from the game Dragon Age: Origins.