Contributed talksPDF document
Bin Packing: From Theory to Experiment and Back AgainIn the bin packing problem, one is given a list of 1-dimensional items and asked to pack them into a minimum number of unit-capacity bins. This was one of the first NP-hard problems to be studied from the "approximation algorithm" point of view, and over the years it has served as a laboratory for the study of new questions about approximation algorithms and the development of new techniques for their analysis. In this talk I present a brief survey of this history, highlighting the many surprising average case behavior results that have been obtained. Several of these surprises were first revealed by experimentation, which led to conjectures and then to proofs, and I will describe this interplay between experimentation and theory. I'll also highlight some as-yet-unproven conjectures suggested by the experimental data.
AI4FM - how to say "why" in proofsThe AI4FM project is exploring how to use AI thinking in discharging proof obligations (POs) that arise in the formal development of programs. Of course, developing better and better heuristics for theorem provers has been explored by AI researchers since its early days. The approach being taken in this project (with Alan Bundy providing the main AI input) is to design a system that can learn from how an expert tackles POs that are beyond current heuristics. We have industrial data that suggests as few as 5 ideas might kill off a hundred undischarged POs. The first step is to design ways of recording the insights which are often about "why" the expert chose a strategy; we will move on to learning such strategies in the next phase of the AI4FM project.
Bio-Inspired Computation Meets Theoretical Computer ScienceBiologically inspired methods of computation such as evolutionary algorithms, ant colony optimisation, particle swarm optimisation etc. are well established in numerous engineering disciplines. As their computational complexity was generally unknown, these approaches lived in the shadows of theoretical computer science for a long time. This dramatically changed in recent years, when bio-inspired computation was finally perceived as a family of algorithms and analysed using methods from classical algorithms and complexity theory.
This talk will present some of the most exciting results that have been obtained in this new research area. We focus on evolutionary algorithms and ant colony optimisation in combinatorial optimisation and prove how they efficiently find optimal or approximate solutions to problems known from the theory of algorithms.