Hybridization of CP and SAT combines the strengths of both paradigms, Constraint Programming (CP) and the Boolean satisfiability problem (SAT). This hybridization allows for the use of dedicated CP propagators paired with the powerful clause learning mechanism of SAT. In contrast to lazy clause generation, solvers based on lazy explanations extract a SAT explanation after each conflict and in particular after those detected by a CP propagator. In this article, we rely on a constraint-wise generic explanation algorithm to build new ad hoc explanation and reason extracting algorithms for the Sum constraint and some of its variants. Time complexity concerns fueled the elaboration of a relaxed version of our ad hoc algorithms, where the loss of a reasonable amount of clause accuracy yields better results. Finally, we conduct an empirical study on XCSP3 instances, where the efficiency of our ad hoc algorithms in reducing the size of generated clauses is clearly visible.

In robust optimization, finding a solution that solely respects the constraints is not enough. Usually, the uncertainty and unknown parameters of the model are represented by random variables. In such conditions, a good solution is a solution robust to most-likely assignments of these random variables. Recently, the Confidence constraint has been introduced by Mercier-Aubin et al. in order to enforce this type of robustness in constraint programming. Unfortunately, it is restricted to a conjunction of binary inequalities In this paper, we generalize the Confidence constraint to any constraint and propose an implementation based on Multi-valued Decision Diagrams (MDDs). The Confidence constraint is defined over a vector of random variables. For a given constraint C, and given a threshold, the Confidence constraint ensures that the probability for C to be satisfied by a sample of the random variables is greater than the threshold. We propose to use MDDs to represent the constraints on the random variables. MDDs are an efficient tool for representing combinatorial constraints, thanks to their exponential compression power. Here, both random and decision variables are stored in the MDD, and propagation rules are proposed for removing values of decision variables that cannot lead to robust solutions. Furthermore, for several constraints, we show that decision variables can be omitted from the MDD because lighter filtering algorithms are sufficient. This leads to gain an exponential factor in the MDD size. The experimental results obtained on a chemical deliveries problem in factories – where the chemicals consumption are uncertain – shows the efficiency of the proposed approach.

In this paper, we propose a model to schedule the next 24 hours of operations in a bulk cargo port to unload bulk cargo trains onto stockpiles. It is a problem that includes multiple parts such as splitting long trains into shorter ones and the routing of bulk material through a configurable network of conveyors to the stockpiles. Managing such trains (up to three kilometers long) also requires specialized equipment. The real world nature of the problem specification implies the necessity to manage heterogeneous data. Indeed, when new equipment is added (e.g. dumpers) or a new type of wagon comes in use, older or different equipment will still be in use as well. In this paper, we provide a detailed presentation of this real world problem and its associated data. This allows us to propose an effective constraint programming model to solve this problem. We also discuss the model design and the different implementations of the propagators that we used in practice. Finally, we show how this model, coupled with a large neighborhood search, was able to find 24 hour schedules efficiently

Heuristics are one of the most important tools to guide search to solve combinatorial problems. They are often specifically designed for one single problem and require both expertise and implementation work. Generic frameworks like SAT or CSP have developed heuristics that obey general principles like first fail or are able to learn and adapt from the exploration of the search tree like Dom/wDeg. In SAT, the classic VSIDS heuristic falls into both categories. The question of whether it is possible to learn from solving existing problems has been addressed for a long time by portfolio solvers where the best heuristic is chosen by Machine Learning from hand-crafted features, and more recently with Deep Learning by embedding this knowledge into a Graph Neural Network (GNN). In this paper, we build upon the latter category by proposing a new heuristic based on Deep Reinforcement Learning using two GNNs with adversarial rewards. We show that our method reduces the number of fails to get the first solution by more than 50% compared to MiniSat. This work shows the advantages of this type of techniques to extract structural and contextual knowledge from past solving experience.

NACRE, for Nogood And Clause Reasoning Engine, is a constraint solver written in C++. It is based on a modular architecture designed to work with generic constraints while implementing several state-of-the-art search methods and heuristics. Interestingly, its data structures have been carefully designed to play around nogoods and clauses, making it suit- able for implementing learning strategies. NACRE was submitted to the CSP MiniTrack of the 2018 and 2019 XCSP3 [8] competitions where it took the first place. This paper gives a general description of NACRE as a framework. We present its kernel, the available search algorithms, and the default settings (notably, used for XCSP3 competitions), which makes NACRE efficient in practice when used as a black-box solver.