Alessandro Previti

AAAI Conference 2026 Conference Paper

On Generating Monolithic and Model Reconciling Explanations in Probabilistic Scenarios (Abstract Reprint)

• Stylianos Loukas Vasileiou
• William Yeoh
• Alessandro Previti
• Tran Cao Son

Explanation generation frameworks aim to make AI systems’ decisions transparent and understandable to human users. However, generating explanations in uncertain environments characterized by incomplete information and probabilistic models remains a significant challenge. In this paper, we propose a novel framework for generating probabilistic monolithic explanations and model reconciling explanations. Monolithic explanations provide self-contained reasons for an explanandum without considering the agent receiving the explanation, while model reconciling explanations account for the knowledge of the agent receiving the explanation. For monolithic explanations, our approach integrates uncertainty by utilizing probabilistic logic to increase the probability of the explanandum. For model reconciling explanations, we propose a framework that extends the logic-based variant of the model reconciliation problem to account for probabilistic human models, where the goal is to find explanations that increase the probability of the explanandum while minimizing conflicts between the explanation and the probabilistic human model. We introduce explanatory gain and explanatory power as quantitative metrics to assess the quality of these explanations. Further, we present algorithms that exploit the duality between minimal correction sets and minimal unsatisfiable sets to efficiently compute both types of explanations in probabilistic contexts. Extensive experimental evaluations on various benchmarks demonstrate the effectiveness and scalability of our approach in generating explanations under uncertainty.

JAIR Journal 2025 Journal Article

On Generating Monolithic and Model Reconciling Explanations in Probabilistic Scenarios

• Stylianos Loukas Vasileiou
• William Yeoh
• Alessandro Previti
• Tran Cao Son

Explanation generation frameworks aim to make AI systems’ decisions transparent and understandable to human users. However, generating explanations in uncertain environments characterized by incomplete information and probabilistic models remains a significant challenge. In this paper, we propose a novel framework for generating probabilistic monolithic explanations and model reconciling explanations. Monolithic explanations provide self-contained reasons for an explanandum without considering the agent receiving the explanation, while model reconciling explanations account for the knowledge of the agent receiving the explanation. For monolithic explanations, our approach integrates uncertainty by utilizing probabilistic logic to increase the probability of the explanandum. For model reconciling explanations, we propose a framework that extends the logic-based variant of the model reconciliation problem to account for probabilistic human models, where the goal is to find explanations that increase the probability of the explanandum while minimizing conflicts between the explanation and the probabilistic human model. We introduce explanatory gain and explanatory power as quantitative metrics to assess the quality of these explanations. Further, we present algorithms that exploit the duality between minimal correction sets and minimal unsatisfiable sets to efficiently compute both types of explanations in probabilistic contexts. Extensive experimental evaluations on various benchmarks demonstrate the effectiveness and scalability of our approach in generating explanations under uncertainty.

AIJ Journal 2023 Journal Article

ASP and subset minimality: Enumeration, cautious reasoning and MUSes

• Mario Alviano
• Carmine Dodaro
• Salvatore Fiorentino
• Alessandro Previti
• Francesco Ricca

Answer Set Programming (ASP) is a well-known logic-based formalism that has been used to model and solve a variety of AI problems. For several years, ASP implementations primarily focused on the main computational task: the computation of one answer set of a (logic) program. Nonetheless, several AI problems, that can be conveniently modelled in ASP, require to enumerate solutions characterized by an optimality property that can be expressed in terms of subset-minimality with respect to some objective atoms. In this context, solutions are often either (i) answer sets that are subset-minimal w. r. t. the objective atoms or (ii) atoms that are contained in all subset-minimal answer sets, or (iii) sets of atoms that enforce the absence of answer sets on the ASP program at hand — such sets are referred to as minimal unsatisfiable subsets (MUSes). In all the above-mentioned cases, the corresponding computational task is currently not supported by plain state-of-the-art ASP solvers. In this paper, we study formally these tasks and fill the gap in current implementations by proposing several algorithms to enumerate MUSes and subset-minimal answer sets, as well as perform cautious reasoning on subset-minimal answer sets. We implement our algorithms on top of wasp and perform an experimental analysis on several hard benchmarks showing the good performance of our implementation.

AAAI Conference 2021 Conference Paper

On Exploiting Hitting Sets for Model Reconciliation

• Stylianos Loukas Vasileiou
• Alessandro Previti
• William Yeoh

In human-aware planning, a planning agent may need to provide an explanation to a human user on why its plan is optimal. A popular approach to do this is called model reconciliation, where the agent tries to reconcile the differences in its model and the human’s model such that the plan is also optimal in the human’s model. In this paper, we present a logicbased framework for model reconciliation that extends beyond the realm of planning. More specifically, given a knowledge base KB1 entailing a formula ϕ and a second knowledge base KB2 not entailing it, model reconciliation seeks an explanation, in the form of a cardinality-minimal subset of KB1, whose integration into KB2 makes the entailment possible. Our approach, based on ideas originating in the context of analysis of inconsistencies, exploits the existing hitting set duality between minimal correction sets (MCSes) and minimal unsatisfiable sets (MUSes) in order to identify an appropriate explanation. However, differently from those works targeting inconsistent formulas, which assume a single knowledge base, MCSes and MUSes are computed over two distinct knowledge bases. We conclude our paper with an empirical evaluation of the newly introduced approach on planning instances, where we show how it outperforms an existing stateof-the-art solver, and generic non-planning instances from recent SAT competitions, for which no other solver exists.

AAAI Conference 2018 Conference Paper

Premise Set Caching for Enumerating Minimal Correction Subsets

• Alessandro Previti
• Carlos Mencía
• Matti Järvisalo
• Joao Marques-Silva

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. Ef- ficient 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.

SAT Conference 2017 Conference Paper

Improving MCS Enumeration via Caching

• Alessandro Previti
• Carlos Mencía
• Matti Järvisalo
• João Marques-Silva 0001

Abstract Enumeration of minimal correction sets (MCSes) of conjunctive normal form formulas is a central and highly intractable problem in infeasibility analysis of constraint systems. Often complete enumeration of MCSes is impossible due to both high computational cost and worst-case exponential number of MCSes. In such cases partial enumeration is sought for, finding applications in various domains, including axiom pinpointing in description logics among others. In this work we propose caching as a means of further improving the practical efficiency of current MCS enumeration approaches, and show the potential of caching via an empirical evaluation.

SAT Conference 2016 Conference Paper

MCS Extraction with Sublinear Oracle Queries

• Carlos Mencía
• Alexey Ignatiev
• Alessandro Previti
• João Marques-Silva 0001

Abstract Given an inconsistent set of constraints, an often studied problem is to compute an irreducible subset of the constraints which, if relaxed, enable the remaining constraints to be consistent. In the case of unsatisfiable propositional formulas in conjunctive normal form, such irreducible sets of constraints are referred to as Minimal Correction Subsets (MCSes). MCSes find a growing number of applications, including the approximation of maximum satisfiability and as an intermediate step in the enumeration of minimal unsatisfiability. A number of efficient algorithms have been proposed in recent years, which exploit a wide range of insights into the MCS extraction problem. One open question is to find the best worst-case number of calls to a SAT oracle, when the calls to the oracle are kept simple, and given reasonable definitions of simple SAT oracle calls. This paper develops novel algorithms for computing MCSes which, in specific settings, are guaranteed to require asymptotically fewer than linear calls to a SAT oracle, where the oracle calls can be viewed as simple. The experimental results, obtained on existing problem instances, demonstrate that the new algorithms contribute to improving the state of the art.

IJCAI Conference 2015 Conference Paper

Literal-Based MCS Extraction

• Carlos Menc
• iacute; a
• Alessandro Previti
• Joao Marques-Silva

Given an over-constrained system, a Maximal Satisfiable Subset (MSS) denotes a maximal set of constraints that are consistent. A Minimal Correction Subset (MCS, or co-MSS) is the complement of an MSS. MSSes/MCSes find a growing range of practical applications, including optimization, configuration and diagnosis. A number of MCS extraction algorithms have been proposed in recent years, enabling very significant performance gains. This paper builds on earlier work and proposes a finer-grained view of the MCS extraction problem, one that reasons in terms of literals instead of clauses. This view is inspired by the relationship between MCSes and backbones of propositional formulas, which is further investigated, and allows for devising a novel algorithm. Also, the paper develops a number of techniques to approximate (weighted partial) MaxSAT by a selective enumeration of MCSes. Empirical results show substantial improvements over the state of the art in MCS extraction and indicate that MCS-based MaxSAT approximation is very effective in practice.

IJCAI Conference 2015 Conference Paper

Prime Compilation of Non-Clausal Formulae

• Alessandro Previti
• Alexey Ignatiev
• Antonio Morgado
• Joao Marques-Silva

Formula compilation by generation of prime implicates or implicants finds a wide range of applications in AI. Recent work on formula compilation by prime implicate/implicant generation often assumes a Conjunctive/Disjunctive Normal Form (CNF/DNF) representation. However, in many settings propositional formulae are naturally expressed in non-clausal form. Despite a large body of work on compilation of non-clausal formulae, in practice existing approaches can only be applied to fairly small formulae, containing at most a few hundred variables. This paper describes two novel approaches for the compilation of non-clausal formulae either with prime implicants or implicates, that is based on propositional Satisfiability (SAT) solving. These novel algorithms also find application when computing all prime implicates of a CNF formula. The proposed approach is shown to allow the compilation of non-clausal formulae of size significantly larger than existing approaches.

SAT Conference 2015 Conference Paper

SAT-Based Formula Simplification

• Alexey Ignatiev
• Alessandro Previti
• João Marques-Silva 0001

Abstract The problem of propositional formula minimization can be traced to the mid of the last century, to the seminal work of Quine and McCluskey, with a large body of work ensuing from this seminal work. Given a set of implicants (or implicates) of a formula, the goal for minimization is to find a smallest set of prime implicants (or implicates) equivalent to the original formula. This paper considers the more general problem of computing a smallest prime representation of a non-clausal propositional formula, which we refer to as formula simplification. Moreover, the paper proposes a novel, entirely SAT-based, approach for the formula simplification problem. The original problem addressed by the Quine-McCluskey procedure can thus be viewed as a special case of the problem addressed in this paper. Experimental results, obtained on well-known representative problem instances, demonstrate that a SAT-based approach for formula simplification is a viable alternative to existing implementations of the Quine-McCluskey procedure.

SAT Conference 2015 Conference Paper

SAT-Based Horn Least Upper Bounds

• Carlos Mencía
• Alessandro Previti
• João Marques-Silva 0001

Abstract Knowledge compilation and approximation finds a wide range of practical applications. One relevant task in this area is to compute the Horn least upper bound (Horn LUB) of a propositional theory F. The Horn LUB is the strongest Horn theory entailed by F. This paper studies this problem and proposes two new algorithms that rely on making successive calls to a SAT solver. The algorithms are analyzed theoretically and evaluated empirically. The results show that the proposed methods are complementary and enable computing Horn LUBs for instances with a non-negligible number of variables.

SAT Conference 2014 Conference Paper

On Computing Preferred MUSes and MCSes

• João Marques-Silva 0001
• Alessandro Previti

Abstract Minimal Unsatisfiable Subsets (MUSes) and Minimal Correction Subsets (MCSes) are essential tools for the analysis of unsatisfiable formulas. MUSes and MCSes find a growing number of applications, that include abstraction refinement in software verification, type debugging, software package management and software configuration, among many others. In some applications, there can exist preferences over which clauses to include in computed MUSes or MCSes, but also in computed Maximal Satisfiable Subsets (MSSes). Moreover, different definitions of preferred MUSes, MCSes and MSSes can be considered. This paper revisits existing definitions of preferred MUSes, MCSes and MSSes of unsatisfiable formulas, and develops a preliminary characterization of the computational complexity of computing preferred MUSes, MCSes and MSSes. Moreover, the paper investigates which of the existing algorithms and pruning techniques can be applied for computing preferred MUSes, MCSes and MSSes. Finally, the paper shows that the computation of preferred sets can have significant impact in practical performance.

ECAI Conference 2014 Conference Paper

Timeout-Sensitive Portfolio Approach to Enumerating Minimal Correction Subsets for Satisfiability Problems

• Yuri Malitsky
• Barry O'Sullivan
• Alessandro Previti
• João Marques-Silva 0001

IJCAI Conference 2013 Conference Paper

On Computing Minimal Correction Subsets

• Joao Marques-Silva
• Federico Heras
• Mikolas Janota
• Alessandro Previti
• Anton Belov

A set of constraints that cannot be simultaneously satisfied is over-constrained. Minimal relaxations and minimal explanations for over-constrained problems find many practical uses. For Boolean formulas, minimal relaxations of over-constrained problems are referred to as Minimal Correction Subsets (MCSes). MCSes find many applications, including the enumeration of MUSes. Existing approaches for computing MCSes either use a Maximum Satisfiability (MaxSAT) solver or iterative calls to a Boolean Satisfiability (SAT) solver. This paper shows that existing algorithms for MCS computation can be inefficient, and so inadequate, in certain practical settings. To address this problem, this paper develops a number of novel techniques for improving the performance of existing MCS computation algorithms. More importantly, the paper proposes a novel algorithm for computing MCSes. Both the techniques and the algorithm are evaluated empirically on representative problem instances, and are shown to yield the most efficient and robust solutions for MCS computation.

AAAI Conference 2013 Conference Paper

Partial MUS Enumeration

• Alessandro Previti
• Joao Marques-Silva

Minimal explanations of infeasibility find a wide range of uses. In the Boolean domain, these are referred to as Minimal Unsatisfiable Subsets (MUSes). In some settings, one needs to enumerate MUSes of a Boolean formula. Most often the goal is to enumerate all MUSes. In cases where this is computationally infeasible, an alternative is to enumerate some MUSes. This paper develops a novel approach for partial enumeration of MUSes, that complements existing alternatives. If the enumeration of all MUSes is viable, then existing alternatives represent the best option. However, for formulas where the enumeration of all MUSes is unrealistic, our approach provides a solution for enumerating some MUSes within a given time bound. The experimental results focus on formulas for which existing solutions are unable to enumerate MUSes, and shows that the new approach can in most cases enumerate a non-negligible number of MUSes within a given time bound.

SAT Conference 2011 Conference Paper

Applying UCT to Boolean Satisfiability

• Alessandro Previti
• Raghuram Ramanujan
• Marco Schaerf
• Bart Selman

Abstract In this paper we perform a preliminary investigation into the application of sampling-based search algorithms to satisfiability testing of propositional formulas in Conjunctive Normal Form (CNF). In particular, we adapt the Upper Confidence bounds applied to Trees (UCT) algorithm [5] which has been successfully used in many game playing programs including MoGo, one of the strongest computer Go players [3].