The uses of machine learning (ML) have snowballed in recent years. In many cases, ML models are highly complex, and their operation is beyond the understanding of human decision-makers. Nevertheless, some uses of ML models involve high-stakes and safety-critical applications. Explainable artificial intelligence (XAI) aims to help human decision-makers in understanding the operation of such complex ML models, thus eliciting trust in their operation. Unfortunately, the majority of past XAI work is based on informal approaches, that offer no guarantees of rigor. Unsurprisingly, there exists comprehensive experimental and theoretical evidence confirming that informal methods of XAI can provide human-decision makers with erroneous information. Logic-based XAI represents a rigorous approach to explainability; it is model-based and offers the strongest guarantees of rigor of computed explanations. However, a well-known drawback of logic-based XAI is the complexity of logic reasoning, especially for highly complex ML models. Recent work proposed distance-restricted explanations, i.e. explanations that are rigorous provided the distance to a given input is small enough. Distance-restricted explainability is tightly related with adversarial robustness, and it has been shown to scale for moderately complex ML models, but the number of inputs still represents a key limiting factor. This paper investigates novel algorithms for scaling up the performance of logic-based explainers when computing and enumerating ML model explanations with a large number of inputs.

Given a machine learning (ML) model and a prediction, explanations can be defined as sets of features which are sufficient for the prediction. In some applications, and besides asking for an explanation, it is also critical to understand whether sensitive features can occur in some explanation, or whether a non-interesting feature must occur in all explanations. This paper starts by relating such queries respectively with the problems of relevancy and necessity in logic-based abduction. The paper then proves membership and hardness results for several families of ML classifiers. Afterwards the paper proposes concrete algorithms for two classes of classifiers. The experimental results confirm the scalability of the proposed algorithms.

Conflict-driven clause learning (CDCL) is at the core of the success of modern SAT solvers. In terms of propositional proof complexity, CDCL has been shown as strong as general resolution. Improvements to SAT solvers can be realized either by improving existing algorithms, or by exploiting proof systems stronger than CDCL. Recent work proposed an approach for solving SAT by reduction to Horn MaxSAT. The proposed reduction coupled with MaxSAT resolution represents a new proof system, DRMaxSAT, which was shown to enable polynomial time refutations of pigeonhole formulas, in contrast with either CDCL or general resolution. This paper investigates the DRMaxSAT proof system, and shows that DRMaxSAT p-simulates general resolution, that AC0-Frege+PHP p-simulates DRMaxSAT, and that DRMaxSAT can not p-simulate AC0-Frege+PHP or the cutting planes proof system.

Model-Based Diagnosis (MBD) finds a growing number of uses in different settings, which include software fault localization, debugging of spreadsheets, web services, and hardware designs, but also the analysis of biological systems, among many others. Motivated by these different uses, there have been significant improvements made to MBD algorithms in recent years. Nevertheless, the analysis of larger and more complex systems motivates further improvements to existing approaches. This paper proposes a novel encoding of MBD into maximum satisfiability (MaxSAT). The new encoding builds on recent work on using Propositional Satisfiability (SAT) for MBD, but identifies a number of key optimizations that are very effective in practice. The paper also proposes a new set of challenging MBD instances, which can be used for evaluating new MBD approaches. Experimental results obtained on existing and on the new MBD problem instances, show conclusive performance gains over the current state of the art.

Boolean optimization finds a wide range of application domains, that motivated a number of different organizations of Boolean optimizers since the mid 90s. Some of the most successful approaches are based on iterative calls to an NP oracle, using either linear search, binary search or the identification of unsatisfiable sub-formulas. The increasing use of Boolean optimizers in practical settings raises the question of confidence in computed results. For example, the issue of confidence is paramount in safety critical settings. One way of increasing the confidence of the results computed by Boolean optimizers is to develop techniques for validating the results. Recent work studied the validation of Boolean optimizers based on branch-and-bound search. This paper complements existing work, and develops methods for validating Boolean optimizers that are based on iterative calls to an NP oracle. This entails implementing solutions for validating both satisfiable and unsatisfiable answers from the NP oracle. The work described in this paper can be applied to a wide range of Boolean optimizers, that find application in Pseudo-Boolean Optimization and in Maximum Satisfiability. Preliminary experimental results indicate that the impact of the proposed method in overall performance is negligible.

Several MaxSAT algorithms based on iterative SAT solving have been proposed in recent years. These algorithms are in general the most efficient for real-world applications. Existing data indicates that, among MaxSAT algorithms based on iterative SAT solving, the most efficient ones are core-guided, i.e. algorithms which guide the search by iteratively computing unsatisfiable subformulas (or cores). For weighted MaxSAT, core-guided algorithms exhibit a number of important drawbacks, including a possibly exponential number of iterations and the use of a large number of auxiliary variables. This paper develops two new algorithms for (weighted) MaxSAT that address these two drawbacks. The first MaxSAT algorithm implements core-guided iterative SAT solving with binary search. The second algorithm extends the first one by exploiting disjoint cores. The empirical evaluation shows that core-guided binary search is competitive with current MaxSAT solvers.

Determining the evolutionary history of a given biological data is an important task in biological sciences. Given a set of quartet topologies over a set of taxa, the Maximum Quartet Consistency (MQC) problem consists of computing a global phylogeny that satisfies the maximum number of quartets. A number of solutions have been proposed for the MQC problem, including Dynamic Programming, Constraint Programming, and more recently Answer Set Programming (ASP). ASP is currently the most efficient approach for optimally solving the MQC problem. This paper proposes encoding the MQC problem with pseudo-Boolean (PB) constraints. The use of PB allows solving the MQC problem with efficient PB solvers, and also allows considering different modeling approaches for the MQC problem. Initial results are promising, and suggest that PB can be an effective alternative for solving the MQC problem.