The CPAIOR Master Class is an annual one-day event (which will be held on September 21 this year) to disseminate cutting-edge research in the areas of constraint programming, artificial intelligence, operations research, and the integration of these fields.
Have a look at the detailed program to the Master Class here.
Abstract: Tools for automating decision-making, commonly referred to as solvers, have seen tremendous improvement over the past decades. Nevertheless, as the problems of today are becoming increasingly complex, the limits of solving technology is constantly being challenged, warranting further advancement of the state-of-the-art. The master class gathers the leading experts to present and discuss the latest techniques incorporated in modern solving technology and to explain their remarkable efficiency in solving large and complex problems. A series of talks is planned, each addressing a particular decision/optimisation paradigm.
Johannes Kepler University, Linz, Austria
In 2004 Prof. Armin Biere joined the Johannes Kepler University in Linz, Austria, and since then chairs the Institute for Formal Models and Verification. His primary research interests are applied formal methods, more specifically formal verification of hardware and software, using model checking and related techniques with the focus on developing efficient SAT and SMT solvers. He is the author and co-author of more than 180 papers and served on the program committee of more than 130 international conferences and workshops. His most influential work is his contribution to Bounded Model Checking. Decision procedures for SAT, QBF and SMT, developed by him or under his guidance rank at the top many international competitions and were awarded 67 medals including 37 gold medals. He is a recipient of an IBM faculty award in 2012, received the TACAS most influential paper in the first 20 years of TACAS in 2014 award, the HVC'15 award on the most influential work in the last five years in formal verification, simulation, and testing, the ETAPS 2017 Test of Time Award, the CAV Award in 2018, and the IJCAI-JAIR 2019 Award.
This tutorial covers algorithmic aspects of conflict-driven clause learning and important extensions developed in recent years, including decision heuristics, restart schemes, various pre- and inprocessing techniques as well as proof generation and checking. Programmatic incremental usage of SAT solvers is discussed next. The talk closes with an overview on the state-of-the-art in parallel SAT solving and open challenges in general.
University of Lisbon, Portugal
Inês Lynce is an associate professor at IST - Universidade de Lisboa and a senior researcher at INESC-ID. She is a well-established researcher in the area of Boolean constraint solving and optimization. Her main contributions refer to the development of search algorithms and the application of those algorithms to solve practical problems. Ines was program co-chair of SAT 2019.
The most well-known optimisation version of the SAT problem is the Maximum Satisfiability (MaxSAT) problem. This talk will provide a practical approach to MaxSAT. We will start by illustrating how to encode a problem in MaxSAT. In addition, modern MaxSAT algorithms, that are based on iterative calls to a SAT solver, will be described.
TU Wien, Austria and University of Udine, Italy
Andrea Schaerf received his PhD in Computer Science from 'Sapienza' University of Rome in 1994, where he has been Assistant Professor from 1996 to 1998. From 1998 to 2005 he has been Associate Professor at University of Udine, where starting 2005 he is Full Professor. His main research interests are: Scheduling and Timetabling Problems, Local Search & Metaheuristics for Combinatorial Problems, and Problem Specification Languages and Tools. Starting February 2015 he is the Head of the Bachelor and Master Programs in Management Engineering at University of Udine.
Günther Raidl is Professor at the Institute of Logic and Computation, TU Wien, Austria, and member of the Algorithms and Complexity Group. He received his PhD in 1994 and completed his habilitation in Practical Computer Science in 2003 at TU Wien. In 2005 he received a professorship position for combinatorial optimization at TU Wien. His research interests include algorithms and data structures in general and combinatorial optimization in particular, with a specific focus on metaheuristics, mathematical programming, intelligent search methods, and hybrid optimization approaches. His research work typically combines theory and practice for application areas such as scheduling, network design, transport optimization, logistics, and cutting and packing. Günther Raidl is associate editor for the INFORMS Journal on Computing and the International Journal of Metaheuristics and at the editorial board of several journals including Algorithms, Metaheuristics and the Evolutionary Computation. He is co-founder and steering committee member of the annual European Conference on Evolutionary Computation in Combinatorial Optimization (EvoCOP). Since 2016 he is faculty member of the Vienna Graduate School on Computational Optimization. Günther Raidl has co-authored a text book on hybrid metaheuristics and over 170 reviewed articles in scientific journals, books, and conference proceedings. Moreover, he has co-edited 13 books. More information can be found at http://www.ac.tuwien.ac.at/raidl.
In the first part of the talk, we will focus on metaheuristics based on Local Search (aka Neighborhood Search), and in particular we focus on Simulated Annealing, which is recognised as the oldest (1983) metaheuristic technique in the scientific literature. Despite its age, it is still very popular in academic publications and practical applications. We review the basic components of Simulated Annealing and we discuss and classify its uncountable variants, some of which gained their own names and metaphors (Great Deluge, Threshold Accepting, ...). In the second half we will consider metaheuristic approaches for discrete optimization problems that rely on or link to machine learning techniques in order to ``learn how to better optimize''. After observing that this general idea is not that new in the field of metaheuristics and briefly surveying established approaches, we will in particular look at a few more recent combinations of heuristic search and reinforcement learning.
Fair Isaac Germany GmbH
Timo Berthold is a developer of the FICO Xpress MIP solver and a researcher at Zuse Institute Berlin, Research Campus MODAL. Before joining FICO, he was a main developer of the SCIP solver which integrates methods from MIP, SAT, and CP. Timo Berthold is an expert on computational mixed-integer linear and nonlinear programming, on heuristic methods and parallel computing. He has published more than 50 research papers in this field and both his PhD and Diploma thesis have won multiple awards.
Numerically challenging mixed-integer programs (MIPs) appear in many practical applications. In this master class presentation, we will discuss recent advances how to handle or even avoid numerical issues while solving such problems. To this end, we will address the following questions:
To (partially!) answer the last question, we will introduce three techniques: Iterative LP Refinement, MIP Solution Refinement and Learning to Scale. We will discuss their effectiveness in reducing numerical errors and their impact on performance in terms of solver running time.
l'Université Nice Sophia-Antipolis, France
Google Paris, France
Laurent Perron spent 11 years in ILOG after a PhD on parallelism in Constraint Programming. He joined Google in 2008 to be the first member of the OR team. He is Tech Lead of the team, working on applications and the CP-SAT solver. Laurent is the creator and main maintainer of the OR-Tools open source project.
Frédéric Didier joined Google in 2009 after a PhD and a PostDoc in computer science. He is part of the OR team since 2012 and has been mainly working on the implementation of many of the OR-Tools optimization algorithms. Frédéric is the main developer of various graph algorithms (max-flow, min-cost flow), of our linear programming solver GLOP, of our Boolean optimization solver BOP already based on SAT/LP, and since 2016 he is the main developer of CP-SAT.
CP-SAT won all gold medals in the Minizinc challenge in the tracks it participated in the last 3 years. It also proved 5 open problems in the MIPLIB 2017 suite, and improved bounds on a few more. In a sense, it realizes the old dream of having a good MIP solver and a good CP solver in the same engine. In this presentation, we will present how the SAT technology has enabled this merging of the two techniques in a competitive way.
Master class organisers
Emir Demirović, Delft University of Technology, The Netherlands
Andrea Rendl, Satalia
Mohamed Siala, INSA Toulouse and LAAS-CNRS
Please refer your questions about the master class to the dedicated email address rather than directly emailing individual organisers:
master-class@cpaior2020.dbai.tuwien.ac.at