Invited Speakers
Ralph Gomory, Stern School, New York University
From Practice to Theory
In the early 1960’s Ralph Gomory and Paul Gilmore of IBM Research worked on the problem of cutting up the very wide rolls of paper that are produced in paper mills into smaller rolls of usable length. This talk describes the practical problems they faced, and describes how working on and solving these practical problems led to Corner Polyhedra and to a long series of theoretical results about integer and mixed integer programming.
Peter van Beek
Constraint Programming in Compiler Optimization: Lessons Learned
Instruction scheduling and instruction selection are two optimization problems that arise in compilers. These problems are considered intractable, and heuristic approaches are currently used in production compilers. In contrast, we have pursued constraint programming approaches that are fast and optimal. The primary goals of this application-driven research were twofold: (i) find solutions of significantly higher quality, and (ii) develop novel constraint programming techniques which have general applicability to similar optimization problems. In this talk, I will describe how successful we were in achieving these goals and some of the lessons we learned along the way.
Bio: Peter van Beek received his PhD in 1990 from the University of Waterloo and at that time joined the faculty at the University of Alberta. Ten years later he returned to Waterloo. His research interests span the field of Artificial Intelligence with a focus on representation and reasoning, constraint programming, constraint satisfaction, planning, sequencing, and scheduling. He has co-authored six research papers which have won awards, and he has served on the program committees of many conferences and on the editorial boards of several journals, including Editor-in-Chief of the journal Constraints. In 2008, Peter van Beek was named a Fellow of the Association for Artificial Intelligence.
Andreas Krause
Sequential Decision Making in Experimental Design and Computational Sustainability via Adaptive Submodularity
Solving sequential decision problems under partial observability is a fundamental but notoriously difficult challenge. In this talk, I will introduce the new concept of adaptive submodularity, generalizing the classical notion of submodular set functions to adaptive policies. We prove that if a problem satisfies this property, a simple adaptive greedy algorithm is guaranteed to be competitive with the optimal policy. The concept allows to recover, generalize and extend existing results in diverse applications including sensor management, viral marketing and active learning. In this talk, I will focus on two case studies. In an application to Bayesian experimental design, we show how greedy optimization of a novel adaptive submodular criterion outperforms standard myopic techniques based on information gain and value of information. I will also discuss how adaptive submodularity can help to address problems in computational sustainability by presenting results on conservation planning for three rare species in the Pacific Northwest of the United States.
Bio: Andreas Krause is an Assistant Professor of Computer Science (tenure-track) at ETH Zurich, where he leads the Learning & Adaptive Systems Group (since 2011). Before that he was Assistant Professor of Computer Science at Caltech (2009-2012). He received his Ph.D. and M.Sc. in Computer Science from Carnegie Mellon University (2008) and his Diplom in Computer Science and Mathematics from the Technical University of Munich, Germany (2004). He is a Microsoft Research Faculty Fellow and a Kavli Frontiers Fellow of the US National Academy of Sciences. He received an ERC Starting Investigator grant, the Deutscher Mustererkennungspreis, an NSF CAREER award, the Okawa Foundation Research Grant recognizing top young researchers in telecommunications as well as the ETH Golden Owl teaching award. His research in learning and adaptive systems that actively acquire information, reason and make decisions in large, distributed and uncertain domains, such as sensor networks and the Web received awards at several premier conferences (AAAI, KDD, IPSN, ICML, UAI) and journals (JAIR, JWRPM).
Vijay Saraswat
Scalable Concurrent Application Frameworks for Constraint Solving
Authors: Ashish Sabharwal, Horst Samulowitz, Ben Herta, David Grove, David Cunningham, Bard Bloom, Vijay Saraswat (speaker)
IBM TJ Watson Research Center
http://x10-lang.org/satx10
The only way for software to continue to ride Moore's law is to go parallel and scale out. But how? For the expert in SAT or mixed integer programming, the prospect of having to deal with low-level concurrent programming in MPI, OpenMP or CUDA is unappetizing at best.
In 2004, we started the X10 programming language project at IBM Research with funding from DARPA to address performance and productivity at scale. X10 is a strongly typed, imperative, object-oriented language in the tradition of Java that offers a single, high-level, programming model subsuming MPI (multi-node execution across a cluster), OpenMP (shared memory concurrency within a node) and CUDA.
X10 runs natively (compiled to C++) and within JVMs, on Linux, MacOS, AIX, Cygwin, Blue Gene, on different inter-connects. It has been shown to scale with performance on over 55,000 cores of a Power7 system (HPCC Challenge Award, 2012).
In this talk, we discuss SatX10, a parallel constraint solver framework written in X10, and described in a paper in the Sat 2012 Tools workshop. The source code for SatX10 is available at http://x10-lang.org/satx10.
With a few dozen lines of X10 code it is possible to run in parallel multiple existing (but slightly modified) sequential constraint solvers (written in Java or C/C++), in such a way that they can communicate constraints to each other. Further, with minor modifications it is possible to ensure determinacy.
We discuss the "global load balancing" framework (written in a few hundred lines of X10) that permits (relocatable) user tasks to be efficiently load balanced across a cluster, using a new technique, life-line based work-stealing. In PPoPP 2011 we presented best known efficiency numbers for the unbalanced tree search problem using these ideas. Recently we have improved these results to show 95% + parallel efficiency on over 50K cores.
We believe such support makes X10 ideal for experimenting with parallel portfolio-based solvers in various domains such as SAT or mixed integer programming.
Bio: Vijay Saraswat's research interests lie in logic, constraints, concurrency and programming languages. Amongst many other topics, he has worked on concurrent constraint programming, natural language semantics, visual programming, discrete and continuous reactive programming, and network communities. He (co-) initiated the work on the X10 programming language in 2004, and has (co-) led the project since. Vijay is a Research Staff Member at IBM TJ Watson, and manages the Advanced Programming Languages department.
Carlos Ansotegui
Tutorial: Recent Advances in Maximum Satisfiability and Extensions
The Maximum Satisfiability (MaxSAT) problem is a generalization of the Satisfiability problem. The idea is that sometimes not all restrictions of a problem can be satisfied, and we try to satisfy the maximum number of them. The MaxSAT problem is a natural combinatorial optimization problem, and the technology developed for its resolution can be applied in several domains, such as: scheduling and timetabling problems, FPGA routing, software package installation, design debugging, bioinformatics, probabilistic reasoning, etc. In the last five years, state-of-the-art MaxSAT solvers have experienced a significant advance and they can be applied on industrial problems.
In this tutorial, we will show how to encode optimization problems into MaxSAT. Then, we will study the algorithms behind successful MaxSAT solvers. In particular, we will emphasize algorithms and implementation details that give the best performance on industrial instances. We will also show how to apply other technologies from Satisfiability Modulo Theories (SMT) and Integer Linear Programming (ILP).
Bio: Carlos Ansótegui is currently associate professor at the University of Lleida, Spain. His research interests include: modeling and solving decision and optimization problems, through the application of Constraint Programming techniques. In particular, those from Satisfiability, Satisfiability Modulo Theories or Maximum Satisfiability. He has coauthored several papers on efficient solvers for the MaxSAT problem. These solvers have ranked among the best at the international MaxSAT Evaluation.
