View: session overviewtalk overviewside by side with other conferences
09:00  PRESENTER: Senne Berden ABSTRACT. Many realworld problems can be effectively solved by means of combinatorial optimization. However, appropriate models to give to a solver are not always available, and sometimes must be learned from historical data. Although some research has been done in this area, the task of learning (weighted partial) MAXSAT models has not received much attention thus far, even though such models can be used in many realworld applications. Furthermore, most existing work is limited to learning models from noncontextual data, where instances are labeled as solutions and nonsolutions, but without any specification of the contexts in which those labels apply. A recent approach named HASSLESLS has addressed these limitations: it can jointly learn hard constraints and weighted soft constraints from labeled contextual examples. However, it is hindered by long runtimes, as evaluating even a single candidate MAXSAT model requires solving as many models as there are contexts in the training data, which quickly becomes highly expensive when the size of the model increases. In this work, we address these runtime issues. To this end, we make two contributions. First, we propose a faster model evaluation procedure that makes use of knowledge compilation. Second, we propose a genetic algorithm named HASSLEGEN that decreases the number of evaluations needed to find good models. We experimentally show that both contributions improve on the state of the art by speeding up learning, which in turn allows higherquality MAXSAT models to be found within a given learning time budget. 
09:30  Selecting SAT Encodings for PseudoBoolean and Linear Integer Constraints PRESENTER: Felix UlrichOltean ABSTRACT. Many constraint satisfaction and optimisation problems can be solved effectively by encoding them as instances of the Boolean Satisfiability problem (SAT). However, even the simplest types of constraints have many encodings in the literature with widely varying performance, and the problem of selecting suitable encodings for a given problem instance is not trivial. We explore the problem of selecting encodings for pseudoBoolean and linear constraints using a supervised machine learning approach. We show that it is possible to select encodings effectively using a standard set of features for constraint problems; however we obtain better performance with a new set of features specifically designed for the pseudoBoolean and linear constraints. In fact, we achieve good results when selecting encodings for unseen problem classes. Our results compare favourably to AutoFolio when using the same feature set. We discuss the relative importance of instance features to the task of selecting the best encodings, and compare several variations of the machine learning method. 
10:00  Improved Sample Complexity Bounds for BranchandCut PRESENTER: Siddharth Prasad ABSTRACT. The branchandcut algorithm for integer programming has a wide variety of tunable parameters that have a huge impact on its performance, but which are challenging to tune by hand. An increasingly popular approach is to use machine learning to configure these parameters based on a training set of integer programs from the application domain. We bound how large the training set should be to ensure that for any configuration, its average performance over the training set is close to its expected future performance. Our guarantees apply to parameters that control the most important aspects of branchandcut: node selection, branching constraint selection, and cut selection, and are sharper and more general than those from prior research. 
09:00  CSP Beyond Tractable Constraint Languages PRESENTER: Stefan Szeider ABSTRACT. The constraint satisfaction problem (CSP) is among the most studied computational problems. While NPhard, many tractable subproblems have been identified (Bulatov 2017, Zuk 2017). Backdoors, introduced by Williams Gomes and Selman (2003), gradually extend such a tractable class to all CSP instances of bounded distance to the class. Backdoor size provides a natural but rather crude distance measure between a CSP instance and a tractable class. Backdoor depth, introduced by Mählmann, Siebertz, and Vigny (2021) for SAT, is a more refined distance measure, which admits the parallel utilization of different backdoor variables. Bounded backdoor size implies bounded backdoor depth, but there are instances of constant backdoor depth and arbitrarily large backdoor size. Dreier, Ordyniak, and Szeider (2022) provided fixedparameter algorithms for finding backdoors of small depth into Horn and 2CNF. In this paper, we consider backdoor depth for CSP. We consider backdoors w.r.t. tractable subproblems $C_\Gamma$ of the CSP defined by a constraint language $\Gamma$, i.e., where all the constraints use relations from the language $\Gamma$. Building upon Dreier et al.’s gametheoretic approach and their notion of separator obstructions, we show that for any finite, tractable, semiconservative constraint language $\Gamma$, the CSP is fixedparameter tractable parameterized by the backdoor depth into $\Gamma$ plus the domain size. With backdoors of low depth, we reach classes of instances that require backdoors of arbitrary large size. Hence, our results strictly generalize several known results for CSP that are based on backdoor size. 
09:30  ABSTRACT. A constraint language G has nonredundancy f(n) if every instance of CSP(G) with n variables contains at most f(n) nonredundant constraints. If G has maximum arity r then it has nonredundancy O(n^r), but there are notable examples for which this upper bound is far from the best possible. In general, the nonredundancy of constraint languages is poorly understood and little is known beyond the trivial bounds Omega(n) and O(n^r). In this paper, we introduce an elementary algebraic framework dedicated to the analysis of the nonredundancy of constraint languages. This framework relates redundancypreserving reductions between constraint languages to closure operators known as pattern partial polymorphisms, which can be interpreted as generic mechanisms to generate redundant constraints in CSP instances. We illustrate the power of this framework by deriving a simple characterisation of languages of arity r having nonredundancy Theta(n^r). 
10:00  FixedTemplate Promise Model Checking Problems PRESENTER: Kristina Asimi ABSTRACT. The fixedtemplate constraint satisfaction problem (CSP) can be seen as the problem of deciding whether a given primitive positive firstorder sentence is true in a fixed structure (also called model). We study a class of problems that generalizes the CSP simultaneously in two directions: we fix a set L of quantifiers and Boolean connectives, and we specify two versions of each constraint, one strong and one weak. Given a sentence which only uses symbols from L, the task is to distinguish whether the sentence is true in the strong sense, or it is false even in the weak sense. We classify the computational complexity of these problems for the existential positive equalityfree fragment of the firstorder logic, i.e., L={∃,∧,∨}, and we prove some upper and lower bounds for the positive equalityfree fragment, L={∃,∀,∧,∨}. The partial results are sufficient, e.g., for all extensions of the latter fragment. 
Lunch will be held in Taub lobby (CP, LICS, ICLP) and in The Grand Water Research Institute (KR, FSCD, SAT).
14:00  Solving with Provably Correct Results: Beyond Satisfiability, and Towards Constraint Programming PRESENTER: Ciaran McCreesh ABSTRACT. Nowadays, Boolean Satisfiability (SAT) solvers aren't allowed to just assert that an instance is unsatisfiable: they're expected to also produce an independently verifiable proof that backs up this claim. This socalled proof logging has done wonders for solver reliability, and has also helped with social acceptability of computergenerated mathematical results. What if we could do the same for constraint programming, producing an auditable solving process where people whose lives or livelihoods are affected by a computer's decision would no longer have to resort to hoping that the system is free of bugs? We will start this tutorial by explaining what a proof really is, and what it means for an algorithm to certify the correctness of its answers by using proof logging. We will give a brief overview of the (extended) resolution and DRAT proof systems used in SAT proof logging. Then we will look at what is needed to bring proof logging to a broader range of solving algorithms, starting with some subgraphfinding algorithms, and moving towards a full CP solver with multiple global constraints and even some reformulation. We will show, by example, what you need to do to use this technology in your own algorithms, and how this relates to the underlying proof methods. We'll finish by discussing how proof logging can also support advanced solving techniques such as symmetry breaking. Surprisingly, all of this can be done in a simple proof format known as "cutting planes with strengthening" that does not know anything about nonbinary variables, global constraints, graphs, groups, or symmetries.

14:00  Trajectory Optimization for Safe Navigation in Maritime Traffic Using Historical Data PRESENTER: Chaithanya Basrur ABSTRACT. Increasing maritime trade often results in congestion in busy ports, thereby necessitating planning methods to avoid close quarter situations among vessels for safer navigation. Rapid digitization and automation of port operations and vessel navigation provide unique opportunities for significantly improving the navigation safety. Our key contributions are as follows. \textit{First}, given a set of future candidate trajectories for vessels involved in a traffic hotspot zone, we develop a multiagent trajectory optimization method to choose trajectories that result in the best overall close quarter risk reduction. Our novel MILPbased trajectory optimization method is more than an orderofmagnitude faster than a standard MILP for this problem, and runs in near realtime. \textit{Second}, although automation has improved in maritime traffic, current vessel traffic systems (in our case study of a busy Asian port) predict only a \textit{single} future trajectory of a vessel based on linear extrapolation. Therefore, using historical data, we learn a \textit{generative model} that predicts \textit{multiple} possible future trajectories of each vessel in a given traffic hotspot area, reflecting past movement patterns of vessels, and integrate it with our trajectory optimizer. \textit{Third}, we validate both our trajectory optimization and generative model extensively using a real world maritime traffic dataset containing 1.7 million trajectories over 1.5 years from one of the busiest ports in the world demonstrating effective risk reduction. 
14:30  PRESENTER: Raphaël Boudreault ABSTRACT. Ship refit projects require ongoing plan management to adapt to arising work and disruptions. Planners must sequence work activities in the best order possible to complete the project in the shortest time or within a defined period while minimizing overtime costs. Activity scheduling must consider milestones, resource availability constraints, and precedence relations. We propose a constraint programming approach for detailed ship refit planning at two granularity levels, daily and hourly schedule. The problem was modeled using the cumulative global constraint, and the SolutionBased Phase Saving heuristic was used to speedup the search, thus achieving the industrialization goals. Based on the evaluation of seven realistic instances over three objectives, the heuristic strategy proved to be significantly faster to find better solutions than using a baseline search strategy. The method was integrated into Refit Optimizer, a cloudbased prototype solution that can import projects from Primavera P6 and optimize plans. 
15:00  PRESENTER: Timothy Curry ABSTRACT. Software defined networks (SDNs) define a programmable network fabric that can be reconfigured to respect global networks properties. Securing against adversaries who try to exploit the network is an objective that conflicts with providing functionality. This paper proposes a twostage mixedinteger programming framework. The first stage automates routing decisions for the flows to be carried by the network while maximizing readability and ease of use for network engineers. The second stage is meant to quickly respond to security breaches to automatically decide on network countermeasures to block the detected adversary. Both stages are computationally challenging and the security stage leverages large neighborhood search to quickly deliver effective response strategies. The approach is evaluated on synthetic networks of various sizes and shown to be effective for both its functional and security objectives. 
16:00  PRESENTER: Simon de Givry ABSTRACT. While processor frequency stagnates for two decades, the number of available cores in servers or clusters is still growing, offering the opportunity for significant speedup in combinatorial optimization. Parallelization of exact methods remains a difficult challenge. We revisit the concept of parallel branchandbound in the framework of weighted constraint satisfaction problems. We show how to adapt an anytime hybrid bestfirst search algorithm in a master/worker protocol. The resulting parallel algorithm achieves a good loadbalancing without introducing new parameters to be tuned as in the embarrassingly parallel search (EPS) approach. It has also a small overhead due to its light communication messages. We performed an experimental evaluation on several benchmarks, comparing our parallel algorithm to its sequential version. We observed linear speedup in some cases. Our approach compared favourably to the EPS approach and also a stateoftheart parallel exact integer programming solver. 
16:30  Sequence Variables for Routing Problems PRESENTER: Augustin Delecluse ABSTRACT. Constraint Programming (CP) is one of the most flexible approaches for modeling and solving vehicle routing problems (VRP). This paper proposes the sequence variable domain, that is inspired by the insertion graph and the subset bound domain for set variables. This domain representation, which targets VRP applications, allows for an efficient insertionbased search on a partial tour and the implementation of simple, yet efficient filtering algorithms for constraints that enforce timewindows on the visits and capacities on the vehicles. Experiment results demonstrate the efficiency and flexibility of this CP domain for solving some hard VRP problems, including the Dial A Ride, the Patient Transportation, and the asymmetric TSP with time windows. 
17:00  PRESENTER: Anthony Karahalios ABSTRACT. We present an exact algorithm for graph coloring and maximum clique problems based on SAT technology. It relies on four subalgorithms that alternatingly compute cliques of larger size and colorings with fewer colors. We show how these techniques can mutually help each other: larger cliques facilitate finding smaller colorings, which in turn can boost finding larger cliques. We evaluate our approach on the DIMACS graph coloring suite, and first show that our algorithm can improve the stateoftheart MaxSATbased solver IncMaxCLQ for finding maximum cliques. For the graph coloring problem, we close two open instances, decrease two upper bounds, and increase one lower bound. 
16:0017:00: Tutorial
17:0017:30: Machine Learning
16:00  Building a Constraint Programming Solver Guided by Machine Learning: Opportunities and Challenges PRESENTER: LouisMartin Rousseau ABSTRACT. In the last years, deep reinforcement learning (DRL) has shown its promise for designing good heuristics dedicated to solve NPhard combinatorial optimization problems. Many recent papers proposed to use directly a learned heuristic to solve the problem in an endtoend fashion. However, such an approach has two shortcomings: (1) it only provides an approximate solution with no systematic ways to improve it nor to prove optimality, (2) it is often limited to standard academic problems (e.g., the travelling salesman problem) and has difficulties to handle complex combinatorial constraints that are present in realistic problems. Constraint programming (CP), as we known, is a generic tool to solve combinatorial optimization problems. Given enough time, its complete search procedure will always find the optimal solution. However, a critical design choice, that makes CP nontrivial to use in practice, is the branching strategy that controls how the space is explored. In this tutorial, we will show how this strategy can be delegated to a DRL agent. First, we will present an initial proof of concept, showing that a CP solver can successfully leverage a learned heuristic. However, the implementation of this prototype suffers from severe inefficiencies issues regarding the execution time. The main reason is that existing CP solvers were not designed to handle learning components in its core engine. This brings the motivation to build a new CP solver, with a direct support for learning heuristics. We will then present SeaPearl, a new opensource CP solver in Julia that has been designed on this purpose, together with the design choices we made. We will also highlight the different challenges that we are currently encountering and preliminary results. 
17:00  Combining Reinforcement Learning and Constraint Programming for SequenceGeneration Tasks with Hard Constraints PRESENTER: Daphné Lafleur ABSTRACT. While Machine Learning (ML) techniques are good at generating data similar to a dataset, they lack the capacity to enforce constraints. On the other hand, any solution to a Constraint Programming (CP) model satisfies its constraints but has no obligation to imitate a dataset. Yet, we sometimes need both. In this paper we borrow RLTuner, a Reinforcement Learning (RL) algorithm introduced to tune neural networks, as our enabling architecture to exploit the respective strengths of ML and CP. RLTuner maximizes the sum of a pretrained network's learned probabilities and of manuallytuned penalties for each violated constraint. We replace the latter with outputs of a CP model representing the marginal probabilities of each note and the number of constraint violations. As was the case for the original RLTuner, we apply our algorithm to music generation since it is a highlyconstrained domain for which CP is especially suited. We show that combining ML and CP, as opposed to using them individually, allows the agent to reflect the pretrained network while taking into account constraints, leading to melodic lines that respect both the corpus' style and the music theory constraints. 