Naar efficiënte en gebruiksgerichte verklaringen voor constraint solving

Constraint solving is a subfield of Artificial Intelligence (AI), where users declaratively state a model of their problem using variables and constraints, and use a constraint solver to compute a solution to their problem. These days, constraint solvers have become extremely efficient, allowing them to be used in several industrial applications, including scheduling, allocation, and time-tabling problems. Indeed, modern solvers are able to solve problems with thousands of variables and constraints, thereby considering millions of alternative solutions in a matter of seconds. However, because of the scale and complexity of these problems, it is often unclear to a user why exactly a solver produced a certain answer. This is especially the case when the solver decides no solution is possible, and the user wants to understand why, or even needs to debug the model. The field of eXplainable Constraint Solving (XCS) focuses exactly on this problem: how to explain the answers of a constraint solver to an end-user. We consider two main challenges for computing explanations in the context of constraint solving: efficient computation, and tailoring the explanation to the user in question by refining the level of detail and providing visualizations. In addition to a set of algorithmic improvements, we investigate the use of explanation techniques in an industrial use case. A common type of explanation is to present the user with a subset of the constraint specification. Such a subset can either be a Minimal Unsatisfiable Subset (MUS), which pinpoints to a conflict, or a Minimal Correction Subset (MCS) showing a set of constraints to relax. However, efficiently computing MUSes and MCSes is a major challenge as multiple NP-hard problems have to be solved in sequence. Recent advancements in SAT-solvers and Lazy-Clause Generation solvers have introduced the concept of incremental solving, which allows for solving different subproblems of a constraint specification, without restarting the solver from scratch. This allows for an efficient implementation of many explanation generation algorithms. However, to use incremental solvers for this application, we need to model the half-reification of each constraint. Currently, modeling systems decompose half-reified global constraints into simpler constraints, which restricts the level of reasoning done by the solver and resulting in longer computation times. In our first contribution, we investigate how to reformulate such half-reified global constraints using auxiliary variables instead of decomposing them. In our second contribution, we investigate how to further reduce the computation time of MUS-computation by exploiting symmetric structures in the model. This allows for reducing the number of times a solver is called during the execution of such algorithms, thereby significantly improving the overall runtime of MUS- computation algorithms. Third, we consider how to refine the abstraction level of the explanation. In particular, in some applications, an MUS can consist of too many constraints to comprehend by a user. We, for the first time, apply the framework of step-wise explanations in the setting of explaining why a problem is unsatisfiable. This type of explanation splits up an MUS into a chain of smaller reasoning steps, where each step considers only a small number of constraints and derives a simple fact. We investigate how to compute a step-wise explanation in this more challenging setting, while paying close attention to avoid any redundancy in the explanation sequence. Apart from dealing with redundancy, applying the step-wise explanation framework to the setting of explaining unsatisfiability also raises new concerns regarding scalability. Indeed, algorithms for computing step-wise explanations are tailored to explaining constraint models with a unique solution, which is a much simpler setting. As a fourth contribution, we investigate how to improve the efficiency of computing step-wise explanations by using a solver-generated proof of correctness as a starting point for the explanation. In particular, we investigate a suite of processing techniques to shorten and simplify a proof, intended to be machine-verifiable, into a user-oriented step-wise explanation. Lastly, we investigate the use of explanation techniques in a real-life allocation and scheduling application in the aircraft manufacturing industry. Here, we use explanation techniques to help the operators in resolving disruptions caused by unexpected events such as adverse weather conditions or technical malfunctions. We investigate several explanation techniques, including MUS and MCS computation and constraint relaxations, and demonstrate how these explanations can be easily visualized. This contribution shows the added value of computing and visualizing explanations in real-life applications. Moreover, it shows the potential of explanation techniques beyond the classical setting of explaining a given constraint model, and we generate explanations while the constraint model is in use instead.