We address the fundamental task of computing rigorous, sample-based abductive explanations for machine learning predictions. In this setting, we propose a new class of explanations derived from a generalization of the consensus operation in propositional logic. We prove that these explanations are precisely those that satisfy a monotonicity property ensuring they remain valid as the sample grows. Furthermore, we show that their computation can be performed efficiently. As a direct application, we also show how these explanations can be used to identify necessary and relevant features. The proposed framework provides a robust and scalable approach to formal model-agnostic XAI.

We address the problem of attributing responsibility to individual clauses for the unsatisfiability of a propositional formula. Recent work adopted the Shapley-Shubik power index, proposing a probabilistic approximation algorithm. However, although polynomial, the required number of SAT solver calls becomes impractical when the input formula is not easy to solve. In such cases, it is often possible to enumerate a partial set of minimal unsatisfiable subsets (MUSes) and minimal correction subsets (MCSes). In this paper, we demonstrate that these subsets can be leveraged to efficiently bound and approximate the Shapley-Shubik index. We introduce a framework that exploits the structural information provided by the available sets to derive useful attribution explanations.

Surrogate evaluation is a useful, if not the unique, technique in population-based evolutionary algorithms where exact fitness calculation is too expensive. This situation arises, for example, in Genetic Programming (GP) applied to evolve scheduling priority rules, since the evaluation of a candidate rule amounts to solve a large number of problem instances acting as training set. In this paper, a simplified model is proposed that relies on finding and then exploiting a small set of small problem instances, termed filter, such that the evaluation of a rule on the filter may help to estimate the performance of the same rule in solving the training set. The problem of finding the best filter is formulated as a variant of the optimal subset problem, which is solved by means of a Genetic Algorithm (GA). The surrogate evaluation of a new candidate rule consist in solving the instances of the filter. This model is exploited in combination with a Memetic Genetic Program (MGP); the resulting algorithm is termed Surrogate Model MGP (SM-MGP). An experimental study was performed on the problem of scheduling a set of jobs on a machine with varying capacity over time, denoted (1,Cap(t)||∑Ti). The results of this study provided interesting insights into the problems of filter and rules calculation, and showcase that the priority rules evolved by SM-MGP outperform those evolved by MGP.

Real-life scheduling problems often require computing solutions on-line, due to real-time requirements. In this scenario, greedy algorithms guided by priority rules are of common use. This is the case of the problem of scheduling jobs on a machine with variable capacity and total tardiness minimization, denoted (1, Cap(t)‖ΣTi). Recent work proposed a Genetic Programming (GP) approach for evolving priority rules for this problem, outperforming several well-known classical rules. In this paper, we consider state space search as an alternative framework and propose a new method based on a refined exhaustive enumeration of priority rules. Our approach, termed Systematic Search and Heuristic Evaluation (SSHE), integrates powerful pruning techniques and an efficient heuristic procedure used to evaluate candidate rules. Experimental results indicate that SSHE represents a valuable alternative to GP.

The analysis of inconsistent formulas finds an ever-increasing range of applications, that include axiom pinpointing in description logics, fault localization in software, model-based diagnosis, optimization problems, but also explainability of machine learning models. This paper overviews approaches for analyzing inconsistent formulas, focusing on finding and enumerating explanations of and corrections for inconsistency, but also on solving optimization problems modeled as inconsistent formulas.

Methods for explaining the sources of inconsistency of overconstrained systems find an ever-increasing number of applications, ranging from diagnosis and configuration to ontology debugging and axiom pinpointing in description logics. Efficient enumeration of minimal correction subsets (MCSes), defined as sets of constraints whose removal from the system restores feasibility, is a central task in such domains. In this work, we propose a novel approach to speeding up MCS enumeration over conjunctive normal form propositional formulas by caching of so-called premise sets (PSes) seen during the enumeration process. Contrasting to earlier work, we move from caching unsatisfiable cores to caching PSes and propose a more effective way of implementing the cache. The proposed techniques noticeably improves on the performance of state-of-the-art MCS enumeration algorithms in practice.

Constraint Programming is becoming the preferred solving technology in a variety of application domains. It is not unusual that a CSP modeling some real-life problem is found to be unfeasible or over-constrained. In this scenario, users may be interested in identifying the causes responsible for inconsistency, or in getting some advice so that they can reformulate their problem to render it feasible. This paper is concerned with the latter issue, which plays a very important role in the analysis of over-constrained problems. Concretely, we study the problem of computing a minimal exclusion set of constraints (MESC) from unfeasible CSPs. A MESC is a set-wise minimal set of constraints whose removal makes the original problem feasible. We provide an overview of existing techniques for MESC extraction and consider additional alternatives and optimizations. Our main contribution is the adaptation of one of the best-performing algorithms for SAT to work in CSP. We also integrate a technique that improves its efficiency. The results from an experimental study indicate considerable improvements over the state-of-the-art.

The job-shop scheduling problem with operators is an extension of the classical job-shop scheduling problem where each operation has to be assisted by one operator from a limited set of them. We confront this problem with the objective of obtaining robust schedules and minimizing the make span. In this way the problem becomes more difficult but more interesting from a practical point of view. We propose to solve the problem in three steps. In the first one, the JSP relaxation (without operators) is modeled and solved using a CSOP solver with the objective of minimizing the make span. Then, the solution is modified to include operators, in this step robustness is introduced by means of a set of buffers in the operators sequences. Finally, these buffers are uniformly distributed among the operations that are not involved in a critical path. We have conducted an experimental study showing that the proposed method reaches a good trade-off between robustness and optimality.