In the field of Explainable Constraint Solving, it is common to explain to a user why a problem is unsatisfiable. A recently proposed method for this is to compute a sequence of explanation steps. Such a step-wise explanation shows individual reasoning steps involving constraints from the original specification, that in the end explain a conflict. However, computing a step-wise explanation is computationally expensive, limiting the scope of problems for which it can be used. We investigate how we can use proofs generated by a constraint solver as a starting point for computing step-wise explanations, instead of computing them step-by-step. More specifically, we define a framework of abstract proofs, in which both proofs and step-wise explanations can be represented. We then propose several methods for converting a proof to a step-wise explanation sequence, with special attention to trimming and simplification techniques to keep the sequence and its individual steps small. Our results show our method significantly speeds up the generation of step-wise explanation sequences, while the resulting step-wise explanation has a quality similar to the current state-of-the-art.

The 5G Radio Access Network (RAN) virtualization aims to improve network quality and lower the operator's costs. One of its main features is the functional split, i.e., dividing the instantiation of RAN baseband functions into different units over metro-network nodes. However, its optimal placement is non-trivial: it depends on the application requirements and on the expected traffic volume, whose daily variation highly impacts the total power consumption. Current optimization solutions fail to provide a placement solution capable of handling traffic fluctuations. In fact, the standard machine learning algorithms used in the literature for planning the network resources in advance result in an allocation that is inadequate to carry the actual traffic at all the time-slots. Hence, we must reserve an artificial buffer capacity in the nodes to ensure feasibility. Instead, our proposed method exploits a fine-grained two-step multi-task algorithm that predicts the mean and quantile traffic, making the artificial capacity no longer necessary. The subsequent placement uses mixed-integer linear programming and a heuristic. The former considers the expected traffic in the objective function (to estimate costs) and the quantile in the constraints (to enforce capacity limits). The heuristic combines the mean and quantile results to minimize the power and comply with the requirements. While using sufficiently large artificial buffers guarantees robustness with a mild power increase compared to the oracle, the fine-grained multi-task model improves the results, reducing the power consumption compared to the mean and meets all constraints. The heuristic enables significant computational time reduction.