publications

2024

1. Delivering Inflated Explanations Yacine Izza, Alexey Ignatiev, Peter J. Stuckey, and Joao Marques-Silva 38th AAAI Conference on Artificial Intelligence (AAAI 2024), pp. 12744–12753, 2024 [Abs] [HTML] [PDF]

   In the quest for Explainable Artificial Intelligence (XAI) one of the questions that frequently arises given a decision made by an AI system is, “why was the decision made in this way?” Formal approaches to explainability build a formal model of the AI system and use this to reason about the properties of the system. Given a set of feature values for an instance to be explained, and a resulting decision, a formal abductive explanation is a set of features, such that if they take the given value will always lead to the same decision. This explanation is useful, it shows that only some features were used in making the final decision. But it is narrow, it only shows that if the selected features take their given values the decision is unchanged. It is possible that some features may change values and still lead to the same decision. In this paper we formally define inflated explanations which is a set of features, and for each feature a set of values (always including the value of the instance being explained), such that the decision will remain unchanged, for any of the values allowed for any of the features in the (inflated) abductive explanation. Inflated formal explanations are more informative than common abductive explanations since e.g. they allow us to see if the exact value of a feature is important, or it could be any nearby value. Overall they allow us to better understand the role of each feature in the decision. We show that we can compute inflated explanations for not that much greater cost than abductive explanations, and that we can extend duality results for abductive explanations also to inflated explanations.

2. SuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-Based, and SAT Techniques E. Albert, M. Garcia Banda, A. Hernández-Cerezo, A. Ignatiev, A. Rubio, and P. J. Stuckey Programming Language Design and Implementation (PLDI 2024) Proceedings of the ACM on Programming Languages, vol. 8, pp. 1437–1462, 2024 [Abs] [HTML] [PDF]

   Given a loop-free sequence of instructions, superoptimization techniques use a constraint solver to search for an equivalent sequence that is optimal for a desired objective. The complexity of the search grows exponentially with the length of the solution being constructed, and the problem becomes intractable for large sequences of instructions. This paper presents a new approach to superoptimizing stack-bytecode via three novel components: (1) a greedy algorithm to refine the bound on the length of the optimal solution; (2) a new representation of the optimization problem as a set of weighted soft clauses in MaxSAT; (3) a series of domain-specific dominance and redundant constraints to reduce the search space for optimal solutions. We have developed a tool, named SuperStack, which can be used to find optimal code translations of modern stack-based bytecode, namely WebAssembly or Ethereum bytecode. Experimental evaluation on more than 500,000 sequences shows the proposed greedy, constraint-based and SAT combination is able to greatly increase optimization gains achieved by existing superoptimizers and reduce to at least a fourth the optimization time.

3. A Formal Explainer for Just-In-Time Defect Predictions Jinqiang Yu, Michael Fu, Alexey Ignatiev, Chakkrit Tantithamthavorn, and Peter J. Stuckey ACM Transactions on Software Engineering and Methodology, vol. xx, pp. xx–xx, 2024 [Abs] [HTML]

   Just-In-Time (JIT) defect prediction has been proposed to help teams to prioritize the limited resources on the most risky commits (or pull requests), yet it remains largely a black-box, whose predictions are not explainable nor actionable to practitioners. Thus, prior studies have applied various model-agnostic techniques to explain the predictions of JIT models. Yet, explanations generated from existing model-agnostic techniques are still not formally sound, robust, and actionable. In this paper, we propose FoX, a Formal eXplainer for JIT Defect Prediction, which builds on formal reasoning about the behaviour of JIT defect prediction models and hence is able to provide provably correct explanations, which are additionally guaranteed to be minimal. Our experimental results show that FoX is able to efficiently generate provably-correct, robust, and actionable explanations while existing model-agnostic techniques cannot. Our survey study with 54 software practitioners provides valuable insights into the usefulness and trustworthiness of our FoX approach. 86% of participants agreed that our approach is useful, while 74% of participants found it trustworthy. Thus, this paper serves as an important stepping stone towards trustable explanations for JIT models to help domain experts and practitioners better understand why a commit is predicted as defective and what to do to mitigate the risk.

4. Anytime Approximate Formal Feature Attribution Jinqiang Yu, Graham Farr, Alexey Ignatiev, and Peter J. Stuckey 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024) LIPIcs, vol. 305, pp. 28:1–28:23, 2024 [Abs] [PDF] [Slides]

   Widespread use of artificial intelligence (AI) algorithms and machine learning (ML) models on the one hand and a number of crucial issues pertaining to them warrant the need for explainable artificial intelligence (XAI). A key explainability question is: given this decision was made, what are the input features which contributed to the decision? Although a range of XAI approaches exist to tackle this problem, most of them have significant limitations. Heuristic XAI approaches suffer from the lack of quality guarantees, and often try to approximate Shapley values, which is not the same as explaining which features contribute to a decision. A recent alternative is so-called formal feature attribution (FFA), which defines feature importance as the fraction of formal abductive explanations (AXp’s) containing the given feature. This measures feature importance from the view of formally reasoning about the model’s behavior. Namely, given a system of constraints logically representing the ML model of interest, computing an AXp requires finding a minimal unsatisfiable subset (MUS) of the system. It is challenging to compute FFA using its definition because that involves counting over all AXp’s (equivalently, counting over MUSes), although one can approximate it. Based on these results, this paper makes several contributions. First, it gives compelling evidence that computing FFA is intractable, even if the set of contrastive formal explanations (CXp’s), which correspond to minimal correction subsets (MCSes) of the logical system, is provided, by proving that the problem is #P-hard. Second, by using the duality between MUSes and MCSes, it proposes an efficient heuristic to switch from MCS enumeration to MUS enumeration on-the-fly resulting in an adaptive explanation enumeration algorithm effectively approximating FFA in an anytime fashion. Finally, experimental results obtained on a range of widely used datasets demonstrate the effectiveness of the proposed FFA approximation approach in terms of the error of FFA approximation as well as the number of explanations computed and their diversity given a fixed time limit.

5. Towards Universally Accessible SAT Technology Alexey Ignatiev, Zi Li Tan, and Christos Karamanos 27tsh International Conference on Theory and Applications of Satisfiability Testing (SAT 2024) LIPIcs, vol. 305, pp. 4:1–4:11, 2024 [Abs] [PDF] [Slides]

   Boolean satisfiability (SAT) solvers are a family of highly efficient reasoning engines, which are frequently used for solving a large and diverse variety of practical challenges. This applies to multidisciplinary problems belonging to the class NP but also those arising at higher levels of the polynomial hierarchy. Unfortunately, encoding a problem of user’s interest to a (series of) propositional formula(s) in conjunctive normal form (CNF), let alone dealing with a SAT solver, is rarely a simple task even for an experienced SAT practitioner. This situation gets aggravated further when the user has little to no knowledge on the operation of the modern SAT solving technology. In 2018, the PySAT framework was proposed to address the issue of fast and "painless" prototyping with SAT solvers in Python allowing researchers to get SAT-based solutions to their problems without investing substantial time in the development process and yet sacrificing only a little in terms of performance. Since then, PySAT has proved a useful instrument for solving a wide range of practical problems and is now a critical package for the PyPI infrastructure. In the meantime, there have been advances in SAT solving and enhancements to PySAT functionality to extend its modelling and solving capabilities in order to make modern SAT technology accessible and deployable on a massive scale. This paper provides a high-level overview of the current architecture of PySAT and some of its capabilities including arbitrary Boolean formula manipulation, CNF preprocessing, and support for external user-defined propagators.

6. Distance-Restricted Explanations: Theoretical Underpinnings & Efficient Implementation Y. Izza, X. Huang, A. Morgado, J. Planes, A. Ignatiev, and J. Marques-Silva 21st Conference on Principles of Knowledge Representation and Reasoning (KR 2024), pp. xx–xx, 2024 [Abs]

   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.

2023

1. From Formal Boosted Tree Explanations to Interpretable Rule Sets Jinqiang Yu, Alexey Ignatiev, and Peter J. Stuckey 29th International Conference on Principles and Practice of Constraint Programming (CP 2023) LIPIcs, vol. 280, pp. 38:1–38:21, 2023 [Abs]

   The rapid rise of Artificial Intelligence (AI) and Machine Learning (ML) has invoked the need for explainable AI (XAI). One of the most prominent approaches to XAI is to train rule-based ML models, e.g. decision trees, lists and sets, that are deemed interpretable due to their transparent nature. Recent years have witnessed a large body of work in the area of constraints- and reasoning-based approaches to the inference of interpretable models, in particular decision sets (DSes). Despite being shown to outperform heuristic approaches in terms of accuracy, most of them suffer from scalability issues and often fail to handle large training data, in which case no solution is offered. Motivated by this limitation and the success of gradient boosted trees, we propose a novel anytime approach to producing DSes that are both accurate and interpretable. The approach makes use of the concept of a generalized formal explanation and builds on the recent advances in formal explainability of gradient boosted trees. Experimental results obtained on a wide range of datasets, demonstrate that our approach produces DSes that more accurate than those of the state-of-the-art algorithms and comparable with them in terms of explanation size.

2. On Computing Probabilistic Abductive Explanations Y. Izza, X. Huang, A. Ignatiev, N. Narodytska, M. C. Cooper, and J. Marques-Silva International Journal of Approximate Reasoning, vol. 159, pp. xx–xx, 2023 [Abs] [HTML]

   The most widely studied explainable AI (XAI) approaches are unsound. This is the case with well-known model-agnostic explanation approaches, and it is also the case with approaches based on saliency maps. One solution is to consider intrinsic interpretability, which does not exhibit the drawback of unsoundness. Unfortunately, intrinsic interpretability can display unwieldy explanation redundancy. Formal explainability represents the alternative to these non-rigorous approaches, with one example being PI-explanations. Unfortunately, PI-explanations also exhibit important drawbacks, the most visible of which is arguably their size. Recently, it has been observed that the (absolute) rigor of PI-explanations can be traded off for a smaller explanation size, by computing the so-called relevant sets. Given some positive δ, a set 𝒮 of features is δ-relevant if, when the features in 𝒮 are fixed, the probability of getting the target class exceeds δ. However, even for very simple classifiers, the complexity of computing relevant sets of features is prohibitive, with the decision problem being NP^PP-complete for circuit-based classifiers. In contrast with earlier negative results, this paper investigates practical approaches for computing relevant sets for a number of widely used classifiers that include Decision Trees (DTs), Naive Bayes Classifiers (NBCs), and several families of classifiers obtained from propositional languages. Moreover, the paper shows that, in practice, and for these families of classifiers, relevant sets are easy to compute. Furthermore, the experiments confirm that succinct sets of relevant features can be obtained for the families of classifiers considered.

3. On Tackling Explanation Redundancy in Decision Trees Yacine Izza, Alexey Ignatiev, and Joao Marques-Silva 32nd International Joint Conference on Artificial Intelligence (IJCAI 2023), pp. 6900–6904, 2023 [Abs] [HTML]

   Claims about the interpretability of decision trees can be traced back to the origins of machine learning (ML). Indeed, given some input consistent with a decision tree’s path, the explanation for the resulting prediction consists of the features in that path. Moreover, a growing number of works propose the use of decision trees, and of other so-called interpretable models, as a possible solution for deploying ML models in high-risk applications. This paper overviews recent theoretical and practical results which demonstrate that for most decision trees, tree paths exhibit so-called explanation redundancy, in that logically sound explanations can often be significantly more succinct than what the features in the path dictates. More importantly, such decision tree explanations can be computed in polynomial-time, and so can be produced with essentially no effort other than traversing the decision tree. The experimental results, obtained on a large range of publicly available decision trees, demonstrate that path explanation redundancy is indeed ubiquitous.

4. No Silver Bullet: Interpretable ML Models Must Be Explained Joao Marques-Silva and Alexey Ignatiev Frontiers in Artificial Intelligence, vol. 6, pp. 1–15, 2023 [Abs] [HTML]

   Recent years witnessed a number of proposals for the use of so-called interpretable models in specific application domains. These include high-risk, but also safety-critical domains. In contrast, other works reported some pitfalls of machine learning model interpretability, in part justified by the lack of a rigorous definition of what an interpretable model should represent. This paper proposes to relate interpretability with the ability of a model to offer explanations of why a prediction is made given some point in feature space. Under this general goal of offering explanations to predictions, the paper reveals additional limitations of interpretable models. Concretely, the paper considers application domains where the purpose is to help human decision makers to understand why some prediction was made or why wasn’t some other prediction made, and where irreducible (and so minimal) information is sought. In such domains, the paper argues that answers to such why (or why not) questions can exhibit arbitrary redundancy, i.e. the answers can be simplified, as long as these answers are obtained by human inspection of the interpretable ML model representation.

5. Eliminating The Impossible, Whatever Remains Must Be True Jinqiang Yu, Alexey Ignatiev, Peter J. Stuckey, Nina Narodytska, and Joao Marques-Silva 37th AAAI Conference on Artificial Intelligence (AAAI 2023), pp. 4123–4131, 2023 [Abs] [arXiv] [HTML] [PDF] [Code]

   The rise of AI methods to make predictions and decisions has led to a pressing need for more explainable artificial intelligence (XAI) methods. One common approach for XAI is to produce a post-hoc explanation, explaining why a black box ML model made a certain prediction. Formal approaches to post-hoc explanations provide succinct reasons for why a prediction was made, as well as why not another prediction was made. But these approaches assume that features are independent and uniformly distributed. While this means that “why” explanations are correct, they may be longer than required. It also means the “why not” explanations may be suspect as the counterexamples they rely on may not be meaningful. In this paper, we show how one can apply background knowledge to give more succinct “why” formal explanations, that are presumably easier to interpret by humans, and give more accurate “why not” explanations. In addition, we show how to use existing rule induction techniques to efficiently extract background information from a dataset.

2022

1. On Tackling Explanation Redundancy in Decision Trees Yacine Izza, Alexey Ignatiev, and Joao Marques-Silva Journal of Artificial Intelligence Research, vol. 75, pp. 261–321, 2022 [Abs] [HTML]

   Decision trees (DTs) epitomize the ideal of interpretability of machine learning (ML) models. The interpretability of decision trees motivates explainability approaches by so-called intrinsic interpretability, and it is at the core of recent proposals for applying interpretable ML models in high-risk applications. The belief in DT interpretability is justified by the fact that explanations for DT predictions are generally expected to be succinct. Indeed, in the case of DTs, explanations correspond to DT paths. Since decision trees are ideally shallow, and so paths contain far fewer features than the total number of features, explanations in DTs are expected to be succinct, and hence interpretable. This paper offers both theoretical and experimental arguments demonstrating that, as long as interpretability of decision trees equates with succinctness of explanations, then decision trees ought not be deemed interpretable. The paper introduces logically rigorous path explanations and path explanation redundancy, and proves that there exist functions for which decision trees must exhibit paths with explanation redundancy that is arbitrarily larger than the actual path explanation. The paper also proves that only a very restricted class of functions can be represented with DTs that exhibit no explanation redundancy. In addition, the paper includes experimental results substantiating that path explanation redundancy is observed ubiquitously in decision trees, including those obtained using different tree learning algorithms, but also in a wide range of publicly available decision trees. The paper also proposes polynomial-time algorithms for eliminating path explanation redundancy, which in practice require negligible time to compute. Thus, these algorithms serve to indirectly attain irreducible, and so succinct, explanations for decision trees. Furthermore, the paper includes novel results related with duality and enumeration of explanations, based on using SAT solvers as witness-producing NP-oracles.

2. Using MaxSAT for Efficient Explanations of Tree Ensembles Alexey Ignatiev, Yacine Izza, Peter J. Stuckey, and Joao Marques-Silva 36th AAAI Conference on Artificial Intelligence (AAAI 2022), pp. 3776–3785, 2022 [Abs] [HTML] [PDF] [Poster] [Slides] [Code]

   Tree ensembles (TEs) denote a prevalent machine learning model that do not offer guarantees of interpretability, that represent a challenge from the perspective of explainable artificial intelligence. Besides model agnostic approaches, recent work proposed to explain TEs with formally-defined explanations, which are computed with oracles for propositional satisfiability (SAT) and satisfiability modulo theories. The computation of explanations for TEs involves linear constraints to express the prediction. In practice, this deteriorates scalability of the underlying reasoners. Motivated by the inherent propositional nature of TEs, this paper proposes to circumvent the need for linear constraints and instead employ an optimization engine for pure propositional logic to efficiently handle the prediction. Concretely, the paper proposes to use a MaxSAT solver and exploit the objective function to determine a winning class. This is achieved by devising a propositional encoding for computing explanations of TEs. Furthermore, the paper proposes additional heuristics to improve the underlying MaxSAT solving procedure. Experimental results obtained on a wide range of publicly available datasets demonstrate that the proposed MaxSAT-based approach is either on par or outperforms the existing reasoning-based explainers, thus representing a robust and efficient alternative for computing formal explanations for TEs.

3. Tractable Explanations for d-DNNF Classifiers X. Huang, Y. Izza, A. Ignatiev, M. C. Cooper, N. Asher, and J. Marques-Silva 36th AAAI Conference on Artificial Intelligence (AAAI 2022), pp. 5719–5728, 2022 [Abs] [HTML] [PDF]

   Compilation into propositional languages finds a growing number of practical uses, including in constraint programming, diagnosis and machine learning (ML), among others. One concrete example is the use of propositional languages as classifiers, and one natural question is how to explain the predictions made. This paper shows that for classifiers represented with some of the best-known propositional languages, different kinds of explanations can be computed in polynomial time. These languages include deterministic decomposable negation normal form (d-DNNF), and so any propositional language that is strictly less succinct than d-DNNF. Furthermore, the paper describes optimizations, specific to Sentential Decision Diagrams (SDDs), which are shown to yield more efficient algorithms in practice.

4. Constraint-Driven Explanations of Black-Box ML Models A. Shrotri, N. Narodytska, A. Ignatiev, K. S. Meel, J. Marques-Silva, and M. Vardi 36th AAAI Conference on Artificial Intelligence (AAAI 2022), pp. 8304–8314, 2022 [Abs] [HTML] [PDF]

   The need to understand the inner workings of opaque Machine Learning models has prompted researchers to devise various types of post-hoc explanations. A large class of such explainers proceed in two phases: first perturb an input instance whose explanation is sought, and then generate an interpretable artifact to explain the prediction of the opaque model on that instance. Recently, Deutch and Frost proposed to use an additional input from the user: a set of constraints over the input space to guide the perturbation phase. While this approach affords the user the ability to tailor the explanation to their needs, striking a balance between flexibility, theoretical rigor and computational cost has remained an open challenge. We propose a novel constraint-driven explanation generation approach which simultaneously addresses these issues in a modular fashion. Our framework supports the use of expressive Boolean constraints giving the user more flexibility to specify the subspace to generate perturbations from. Leveraging advances in Formal Methods, we can theoretically guarantee strict adherence of the samples to the desired distribution. This also allows us to compute fidelity in a rigorous way, while scaling much better in practice. Our empirical study demonstrates concrete uses of our tool CLIME in obtaining more meaningful explanations with high fidelity.

5. Delivering Trustworthy AI through Formal XAI Joao Marques-Silva and Alexey Ignatiev 36th AAAI Conference on Artificial Intelligence (AAAI 2022), pp. 12342–12350, 2022 [Abs] [HTML] [PDF]

   The deployment of systems of artificial intelligence (AI) in high-risk settings warrants the need for trustworthy AI. This crucial requirement is highlighted by recent EU guidelines and regulations, but also by recommendations from OECD and UNESCO, among several other examples. One critical premise of trustworthy AI involves the necessity of finding explanations that offer reliable guarantees of soundness. This paper argues that the best known eXplainable AI (XAI) approaches fail to provide sound explanations, or that alternatively find explanations which can exhibit significant redundancy. The solution to these drawbacks are explanation approaches that offer formal guarantees of rigor. These formal explanations are not only sound but guarantee irredundancy. This paper summarizes the recent developments in the emerging discipline of formal XAI. The paper also outlines existing challenges for formal XAI.

2021

1. A Scalable Two Stage Approach to Computing Optimal Decision Sets Alexey Ignatiev, Edward Lam, Peter J. Stuckey, and Joao Marques-Silva 35th AAAI Conference on Artificial Intelligence (AAAI 2021), pp. 3806–3814, 2021 [Abs] [arXiv] [HTML] [PDF] [Poster] [Slides] [Code]

   Machine learning (ML) is ubiquitous in modern life. Since it is being deployed in technologies that affect our privacy and safety, it is often crucial to understand the reasoning behind its decisions, warranting the need for explainable AI. Rule-based models, such as decision trees, decision lists, and decision sets, are conventionally deemed to be the most interpretable. Recent work uses propositional satisfiability (SAT) solving (and its optimization variants) to generate minimum-size decision sets. Motivated by limited practical scalability of these earlier methods, this paper proposes a novel approach to learn minimum-size decision sets by enumerating individual rules of the target decision set independently of each other, and then solving a set cover problem to select a subset of rules. The approach makes use of modern maximum satisfiability and integer linear programming technologies. Experiments on a wide range of publicly available datasets demonstrate the advantage of the new approach over the state of the art in SAT-based decision set learning.

2. Evaluating the Hardness of SAT Instances Using Evolutionary Optimization Algorithms A. Semenov, D. Chivilikhin, A. Pavlenko, I. Otpuschennikov, V. Ulyantsev, and A. Ignatiev 27th International Conference on Principles and Practice of Constraint Programming (CP 2021) LIPIcs, vol. 210, pp. 47:1–47:18, 2021 [Abs] [HTML]

   Propositional satisfiability (SAT) solvers are deemed to be among the most efficient reasoners, which have been successfully used in a wide range of practical applications. As this contrasts the well-known NP-completeness of SAT, a number of attempts have been made in the recent past to assess the hardness of propositional formulas in conjunctive normal form (CNF). The present paper proposes a CNF formula hardness measure which is close in conceptual meaning to the one based on Backdoor set notion: in both cases some subset B of variables in a CNF formula is used to define the hardness of the formula w.r.t. this set. In contrast to the backdoor measure, the new measure does not demand the polynomial decidability of CNF formulas obtained when substituting assignments of variables from B to the original formula. To estimate this measure the paper suggests an adaptive (ε, δ)-approximation probabilistic algorithm. The problem of looking for the subset of variables which provides the minimal hardness value is reduced to optimization of a pseudo-Boolean black-box function. We apply evolutionary algorithms to this problem and demonstrate applicability of proposed notions and techniques to tests from several families of unsatisfiable CNF formulas.

3. Propositional Proof Systems Based on Maximum Satisfiability Maria Luisa Bonet, Sam Buss, Alexey Ignatiev, Antonio Morgado, and Joao Marques-Silva Artificial Intelligence, vol. 300, pp. xxx–xxx, 2021 [Abs] [HTML]

   The paper describes the use of dual-rail MaxSAT systems to solve Boolean satisfiability (SAT), namely to determine if a set of clauses is satisfiable. The Horn MaxSAT problem is the problem of satisfying the maximum number of clauses in an instance of SAT. The dual-rail encoding adds extra variables for the complements of variables, and allows encoding an instance of SAT as a Horn MaxSAT problem. We discuss three implementations of dual-rail MaxSAT: core-guided systems, minimal hitting set (MaxHS) systems, and Horn MaxSAT resolution inference systems. All three of these can be more efficient than resolution and thus than conflict-driven clause learning (CDCL). All three systems can give polynomial size refutations for the pigeonhole principle, the doubled pigeonhole principle and the mutilated chessboard principles. The dual-rail MaxHS MaxSat system can give polynomial size proofs of the parity principle. However, dual-rail MaxSAT resolution requires exponential size proofs for the parity principle; this is proved by showing that constant depth Frege augmented with the pigeonhole principle can polynomially simulate dual-rail MaxSAT resolution. Consequently, dual-rail MaxSAT resolution does not simulate cutting planes. We further show that core-guided dual-rail MaxSAT and weighted dual-rail MaxSAT resolution polynomially simulate resolution. Finally, we report the results of experiments with core-guided dual-rail MaxSAT and MaxHS dual-rail MaxSAT showing strong performance by these systems.

4. From Contrastive to Abductive Explanations and Back Again — Extended Abstract Alexey Ignatiev, Nina Narodytska, Nicholas Asher, and Joao Marques-Silva 18th Conference on Principles of Knowledge Representation and Reasoning (KR 2021), 2021 [Abs] [arXiv] [PDF] [Poster] [Slides]

   Explanations of Machine Learning models often address a ‘Why?’ question. These can are related with selecting feature-value pairs sufficient for the prediction. Recent work has investigated explanations that address a ‘Why Not?’ question, i.e. finding a change of feature values that guarantees a change of prediction. These two forms of explanations of ML models appear to be mostly unrelated. However, this paper demonstrates otherwise and establishes a rigorous formal relationship between ‘Why?’ and ‘Why Not?’ explanations. The paper proves that for any given instance, ‘Why?’ explanations are minimal hitting sets of ‘Why Not?’ explanations and vice-versa. Moreover, the paper devises novel algorithms for extracting and enumerating both forms of explanations.

5. On Efficiently Explaining Graph-Based Classifiers Xuanxiang Huang, Yacine Izza, Alexey Ignatiev, and Joao Marques-Silva 18th Conference on Principles of Knowledge Representation and Reasoning (KR 2021), pp. 356–367, 2021 [Abs] [arXiv] [HTML] [PDF]

   Recent work has shown that not only decision trees (DTs) may not be interpretable but also proposed a polynomial-time algorithm for computing one PI-explanation of a DT. This paper shows that for a large class of classifiers, globally referred to as decision graphs, and which include decision trees and binary decision diagrams, but also their multi-valued variants, there exist polynomial time algorithms for computing one PI-explanation. In addition, the paper also proposes a polynomial time algorithm for computing one contrastive explanation. These novel algorithms build on explanation graphs (XpG’s). XpG’s denote a graph representation that enables both theoretical and practically efficient computation of explanations for decision graphs. Furthermore, the paper proposes a practically efficient solution for the enumeration of explanations, and studies the complexity ofdeciding whether a given feature is included in some explanation. For the concrete case of decision trees, the paper shows that contrastive explanations can be enumerated in polynomial total time. Finally, the experimental results validate the practical applicability of the algorithms proposed in the paper on a wide range of publicly available benchmarks.

6. Explanations for Monotonic Classifiers J. Marques-Silva, T. Gerspacher, M. C. Cooper, A. Ignatiev, and N. Narodytska 38th International Conference on Machine Learning (ICML 2021) Proceedings of Machine Learning Research, vol. 139, pp. 7469–7479, 2021 [Abs] [arXiv] [HTML] [PDF]

   In many classification tasks there is a requirement of monotonicity. Concretely, if all else remains constant, increasing (resp. decreasing) the value of one or more features must not decrease (resp. increase) the value of the prediction. Despite comprehensive efforts on learning monotonic classifiers, dedicated approaches for explaining monotonic classifiers are scarce and classifier-specific. This paper describes novel algorithms for the computation of one formal explanation of a (black-box) monotonic classifier. These novel algorithms are polynomial (indeed linear) in the run time complexity of the classifier. Furthermore, the paper presents a practically efficient model-agnostic algorithm for enumerating formal explanations.

7. SAT-Based Rigorous Explanations for Decision Lists Alexey Ignatiev and Joao Marques-Silva 24th International Conference on Theory and Applications of Satisfiability Testing (SAT 2021) Lecture Notes in Computer Science, vol. 12831, pp. 251–269, 2021 [Abs] [arXiv] [HTML] [PDF] [Poster] [Slides] [Code]

   Decision lists (DLs) find a wide range of uses for classification problems in Machine Learning (ML), being implemented in a number of ML frameworks. DLs are often perceived as interpretable. However, building on recent results for decision trees (DTs), we argue that interpretability is an elusive goal for some DLs. As a result, for some uses of DLs, it will be important to compute (rigorous) explanations. Unfortunately, and in clear contrast with the case of DTs, this paper shows that computing explanations for DLs is computationally hard. Motivated by this result, the paper proposes propositional encodings for computing abductive explanations (AXps) and contrastive explanations (CXps) of DLs. Furthermore, the paper investigates the practical efficiency of a MARCO-like approach for enumerating explanations. The experimental results demonstrate that, for DLs used in practical settings, the use of SAT oracles offers a very efficient solution, and that complete enumeration of explanations is most often feasible.

8. Assessing Progress in SAT Solvers Through the Lens of Incremental SAT Stepan Kochemazov, Alexey Ignatiev, and Joao Marques-Silva 24th International Conference on Theory and Applications of Satisfiability Testing (SAT 2021) Lecture Notes in Computer Science, vol. 12831, pp. 280–298, 2021 [Abs] [HTML] [PDF] [Code]

   There is a wide consensus, which is supported by the hard experimental evidence of the SAT competitions, that clear progress in SAT solver performance has been observed in recent years. However, in the vast majority of practical applications of SAT, one is expected to use SAT solvers as oracles deciding a possibly large number of propositional formulas. In practice, this is often achieved through the use of incremental SAT. Given this fundamental use of SAT solvers, this paper investigates whether recent improvements in solver performance have an observable positive impact on the overall problem-solving efficiency in settings where incremental SAT is mandatory or at least expected. Our results, obtained on a number of well-known practically significant applications, suggest that most improvements made to SAT solvers in recent years have no positive impact on the overall performance when solvers are used incrementally.

9. Reasoning-Based Learning of Interpretable ML Models Alexey Ignatiev, Joao Marques-Silva, Nina Narodytska, and Peter J. Stuckey 30th International Joint Conference on Artificial Intelligence (IJCAI 2021), 2021 [Abs] [PDF] [Poster] [Slides]

   Artificial Intelligence (AI) is widely used in decision making procedures in myriads of real-world applications across important practical areas such as finance, healthcare, education, and safety critical systems. Due to its ubiquitous use in safety and privacy critical domains, it is often vital to understand the reasoning behind the AI decisions, which motivates the need for explainable AI (XAI). One of the major approaches to XAI is represented by computing so-called interpretable machine learning (ML) models, such as decision trees (DT), decision lists (DL) and decision sets (DS). These models build on the use of if-then rules and are thus deemed to be easily understandable by humans. A number of approaches have been proposed in the recent past to devising all kinds of interpretable ML models, the most prominent of which involve encoding the problem into a logic formalism, which is then tackled by invoking a reasoning or discrete optimization procedure. This paper overviews the recent advances of the reasoning and constraints based approaches to learning interpretable ML models and discusses their advantages and limitations.

10. Optimizing Binary Decision Diagrams for Interpretable Machine Learning Classification G. Cabodi, P. E. Camurati, A. Ignatiev, J. Marques-Silva, M. Palena, and P. Pasini Design, Automation and Test in Europe Conference (DATE 2021), pp. 1122–1125, 2021 [Abs] [HTML] [PDF]

    Motivated by the need to understand the behaviour of complex machine learning (ML) models, there has been recent interest in learning optimal (or sub-optimal) decision trees (DTs). This interest is explained by the fact that DTs are widely regarded as interpretable by human decision makers. An alternative to DTs are Binary Decision Diagrams (BDDs), which can be deemed interpretable. Compared to DTs, and despite a fixed variable order, BDDs offer the advantage of more compact representations in practice, due to node sharing. Moreover, there is also extensive experience in the efficient manipulation of BDDs. Our work proposes preliminary inroads in two main directions: (a) proposing a SAT-based model for computing a decision tree as the smallest Reduced Ordered Binary Decision Diagram, consistent with given training data; and (b) exploring heuristic approaches for deriving sub-optimal (i.e., not minimal) ROBDDs, in order to improve the scalability of the proposed technique. The heuristic approach is related to recent work on using BDDs for classification. Whereas previous works addressed size reduction by general logic synthesis techniques, our work adds the contribution of generalized cofactors, that are a well-known compaction technique specific to BDDs, once a care (or equivalently a don’t care) set is given. Preliminary experimental results are also provided, proposing a direct comparison between optimal and sub-optimal solutions, as well as an evaluation of the impact of the proposed size reduction steps.

11. Learning Optimal Decision Sets and Lists with SAT Jinqiang Yu, Alexey Ignatiev, Peter J. Stuckey, and Pierre Le Bodic Journal of Artificial Intelligence Research, vol. 72, pp. 1251–1279, 2021 [Abs] [HTML]

    Decision sets and decision lists are two examples of the most easily explainable machine learning models. Given the renewed emphasis on explainable machine learning decisions, both of these machine learning models are increasingly attractive, combining small size and clear explainability. Here, we define size as the total number of literals in these rule-based models as opposed to earlier work that concentrates on the number of rules. In this paper, we develop approaches to computing minimum-size "perfect" decision sets and decision lists, which are perfectly accurate on the training data, and minimal in size, making use of modern SAT solving technology. We also provide a new method for determining optimal sparse alternatives, which trade off size and accuracy. The experiments in this paper demonstrate that the optimal decision sets computed by the SAT-based approach are comparable with the best heuristic methods, but much more succinct, and thus, more explainable. We contrast the size and test accuracy of optimal decisions lists versus optimal decision sets, as well as other state-of-the-art methods for determining optimal decision lists. Finally, we examine the size of average explanations generated by decision sets and decision lists.

2020

1. Branch Location Problems with Maximum Satisfiability Oleg Zaikin, Alexey Ignatiev, and Joao Marques-Silva 24th European Conference on Artificial Intelligence (ECAI 2020), pp. 379–386, 2020 [Abs] [HTML] [PDF]

   Constrained location problems find a wide range of practical applications. Recent work showed that dedicated brute-force algorithms and greedy approach enable solutions of reasonable efficiency, for a restriction of the general constrained location problem, referred to as the branch location problem. This paper extends earlier work in several ways. First, the paper develops propositional encodings for the branch location problem. Second, given that the branch location problem is a restriction of the general constraint location problem, the paper shows that the restricted problem is still hard for NP. Third, the paper devises improved propositional encodings for the branch location problem, which in practice enable not only solving exactly a significantly larger class of problems but also effectively approximating optimal problem solutions, using state-of-the-art (complete and incomplete) Maximum Satisfiability (MaxSAT) solvers.

2. Explaining Naive Bayes and Other Linear Classifiers with Polynomial Time and Delay J. Marques-Silva, T. Gerspacher, M. C. Cooper, A. Ignatiev, and N. Narodytska 34th Conference on Neural Information Processing Systems (NeurIPS 2020), 2020 [Abs] [arXiv] [HTML] [PDF] [Code]

   Recent work proposed the computation of so-called PI-explanations of Naive Bayes Classifiers (NBCs). PI-explanations are subset-minimal sets of feature-value pairs that are sufficient for the prediction, and have been computed with state-of-the-art exact algorithms that are worst-case exponential in time and space. In contrast, we show that the computation of one PI-explanation for an NBC can be achieved in log-linear time, and that the same result also applies to the more general class of linear classifiers. Furthermore, we show that the enumeration of PI-explanations can be obtained with polynomial delay. Experimental results demonstrate the performance gains of the new algorithms when compared with earlier work. The experimental results also investigate ways to measure the quality of heuristic explanations.

3. Optimal Decision Lists using SAT Jinqiang Yu, Alexey Ignatiev, Pierre Le Bodic, and Peter J. Stuckey CoRR abs/2010.09919, 2020 [Abs] [HTML]

   Decision lists are one of the most easily explainable machine learning models. Given the renewed emphasis on explainable machine learning decisions, this machine learning model is increasingly attractive, combining small size and clear explainability. In this paper, we show for the first time how to construct optimal "perfect" decision lists which are perfectly accurate on the training data, and minimal in size, making use of modern SAT solving technology. We also give a new method for determining optimal sparse decision lists, which trade off size and accuracy. We contrast the size and test accuracy of optimal decisions lists versus optimal decision sets, as well as other state-of-the-art methods for determining optimal decision lists. We also examine the size of average explanations generated by decision sets and decision lists.

4. On Explaining Decision Trees Yacine Izza, Alexey Ignatiev, and Joao Marques-Silva CoRR abs/2010.11034, 2020 [Abs] [HTML]

   Decision trees (DTs) epitomize what have become to be known as interpretable machine learning (ML) models. This is informally motivated by paths in DTs being often much smaller than the total number of features. This paper shows that in some settings DTs can hardly be deemed interpretable, with paths in a DT being arbitrarily larger than a PI-explanation, i.e. a subset-minimal set of feature values that entails the prediction. As a result, the paper proposes a novel model for computing PI-explanations of DTs, which enables computing one PI-explanation in polynomial time. Moreover, it is shown that enumeration of PI-explanations can be reduced to the enumeration of minimal hitting sets. Experimental results were obtained on a wide range of publicly available datasets with well-known DT-learning tools, and confirm that in most cases DTs have paths that are proper supersets of PI-explanations.

5. Towards Formal Fairness in Machine Learning A. Ignatiev, M. C. Cooper, M. Siala, E. Hebrard, and J. Marques-Silva 26th International Conference on Principles and Practice of Constraint Programming (CP 2020) Lecture Notes in Computer Science, vol. 12333, pp. 846–867, 2020 [Abs] [arXiv] [HTML] [PDF]

   One of the challenges of deploying machine learning (ML) systems is fairness. Datasets often include sensitive features, which ML algorithms may unwittingly use to create models that exhibit unfairness. Past work on fairness offers no formal guarantees in their results. This paper proposes to exploit formal reasoning methods to tackle fairness. Starting from an intuitive criterion for fairness of an ML model, the paper formalises it, and shows how fairness can be represented as a decision problem, given some logic representation of an ML model. The same criterion can also be applied to assessing bias in training data. Moreover, we propose a reasonable set of axiomatic properties which no other definition of dataset bias can satisfy. The paper also investigates the relationship between fairness and explainability, and shows that approaches for computing explanations can serve to assess fairness of particular predictions. Finally, the paper proposes SAT-based approaches for learning fair ML models, even when the training data exhibits bias, and reports experimental trials.

6. Computing Optimal Decision Sets with SAT Jinqiang Yu, Alexey Ignatiev, Peter J. Stuckey, and Pierre Le Bodic 26th International Conference on Principles and Practice of Constraint Programming (CP 2020) Lecture Notes in Computer Science, vol. 12333, pp. 952–970, 2020 [Abs] [arXiv] [HTML] [PDF]

   As machine learning is increasingly used to help make decisions, there is a demand for these decisions to be explainable. Arguably, the most explainable machine learning models use decision rules. This paper focuses on decision sets, a type of model with unordered rules, which explains each prediction with a single rule. In order to be easy for humans to understand, these rules must be concise. Earlier work on generating optimal decision sets first minimizes the number of rules, and then minimizes the number of literals, but the resulting rules can often be very large. Here we consider a better measure, namely the total size of the decision set in terms of literals. So we are not driven to a small set of rules which require a large number of literals. We provide the first approach to determine minimum-size decision sets that achieve minimum empirical risk and then investigate sparse alternatives where we trade accuracy for size. By finding optimal solutions we show we can build decision set classifiers that are almost as accurate as the best heuristic methods, but far more concise, and hence more explainable.

7. Towards Trustable Explainable AI Alexey Ignatiev 29th International Joint Conference on Artificial Intelligence (IJCAI 2020), pp. 5154–5158, 2020 [Abs] [HTML] [PDF] [Poster] [Slides]

   Explainable artificial intelligence (XAI) represents arguably one of the most crucial challenges being faced by the area of AI these days. Although the majority of approaches to XAI are of heuristic nature, recent work proposed the use of abductive reasoning to computing provably correct explanations for machine learning (ML) predictions. The proposed rigorous approach was shown to be useful not only for computing trustable explanations but also for validating explanations computed heuristically. It was also applied to uncover a close relationship between XAI and verification of ML models. This paper overviews the advances of the rigorous logic-based approach to XAI and argues that it is indispensable if trustable XAI is of concern.

8. From Contrastive to Abductive Explanations and Back Again Alexey Ignatiev, Nina Narodytska, Nicholas Asher, and Joao Marques-Silva XIXth International Conference of the Italian Association for Artificial Intelligence (AI*IA 2020) Lecture Notes in Computer Science, vol. 12414, pp. 335–355, 2020 [Abs] [arXiv] [HTML] [PDF]

   Explanations of Machine Learning (ML) models often address a ‘Why?’ question. Such explanations can be related with selecting feature-value pairs which are sufficient for the prediction. Recent work has investigated explanations that address a ‘Why Not?’ question, i.e. finding a change of feature values that guarantee a change of prediction. Given their goals, these two forms of explaining predictions of ML models appear to be mostly unrelated. However, this paper demonstrates otherwise, and establishes a rigorous formal relationship between ‘Why?’ and ‘Why Not?’ explanations. Concretely, the paper proves that, for any given instance, ‘Why?’ explanations are minimal hitting sets of ‘Why Not?’ explanations and vice-versa. Furthermore, the paper devises novel algorithms for extracting and enumerating both forms of explanations.

2019

1. RC2: An Efficient MaxSAT Solver Alexey Ignatiev, Antonio Morgado, and Joao Marques-Silva Journal on Satisfiability, Boolean Modeling and Computation, vol. 11, pp. 53–64, 2019 [Abs] [HTML] [PDF] [Code]

   Recent work proposed a toolkit PySAT aiming at fast and easy prototyping with propositional satisfiability (SAT) oracles in Python, which enabled one to exploit the power of the original implementations of the state-of-the-art SAT solvers in Python. Maximum satisfiability (MaxSAT) is a well-known optimization version of SAT, which can be solved with a series of calls to a SAT oracle. Based on this fact and motivated by the ideas underlying the PySAT toolkit, this paper describes and evaluates RC2 (stands for relaxable cardinality constraints), a new core-guided MaxSAT solver written in Python, which won both unweighted and weighted categories of the main track of MaxSAT Evaluation 2018.

2. Abduction-Based Explanations for Machine Learning Models Alexey Ignatiev, Nina Narodytska, and Joao Marques-Silva 33rd AAAI Conference on Artificial Intelligence (AAAI 2019), pp. 1511–1519, 2019 [Abs] [arXiv] [HTML] [PDF] [Slides]

   The growing range of applications of Machine Learning (ML) in a multitude of settings motivates the ability of computing small explanations for predictions made. Small explanations are generally accepted as easier for human decision makers to understand. Most earlier work on computing explanations is based on heuristic approaches, providing no guarantees of quality, in terms of how close such solutions are from cardinality- or subset-minimal explanations. This paper develops a constraint-agnostic solution for computing explanations for any ML model. The proposed solution exploits abductive reasoning, and imposes the requirement that the ML model can be represented as sets of constraints using some target constraint reasoning system for which the decision problem can be answered with some oracle. The experimental results, obtained on well-known datasets, validate the scalability of the proposed approach as well as the quality of the computed solutions.

3. Model-Based Diagnosis with Multiple Observations Alexey Ignatiev, Antonio Morgado, Georg Weissenbacher, and Joao Marques-Silva 28th International Joint Conference on Artificial Intelligence (IJCAI 2019), pp. 1108–1115, 2019 [Abs] [HTML] [PDF] [Slides] [Code]

   Existing automated testing frameworks require multiple observations to be jointly diagnosed with the purpose of identifying common fault locations. This is the case for example with continuous integration tools. This paper shows that existing solutions fail to compute the set of minimal diagnoses, and as a result run times can increase by orders of magnitude. The paper proposes not only solutions to correct existing algorithms, but also conditions for improving their run times. Nevertheless, the diagnosis of multiple observations raises a number of important computational challenges, which even the corrected algorithms are often unable to cope with. As a result, the paper devises a novel algorithm for diagnosing multiple observations, which is shown to enable significant performance improvements in practice.

4. Efficient Symmetry Breaking for SAT-Based Minimum DFA Inference I. Zakirzyanov, A. Morgado, A. Ignatiev, V. Ulyantsev, and J. Marques-Silva 21st International Conference on Theory and Applications of Satisfiability Testing (LATA 2019) Lecture Notes in Computer Science, vol. 11417, pp. 159–173, 2019 [Abs] [HTML] [PDF]

   Inference of deterministic finite automata (DFA) finds a wide range of important practical applications. In recent years, the use of SAT and SMT solvers for the minimum size DFA inference problem (MinDFA) enabled significant performance improvements. Nevertheless, there are many problems that are simply too difficult to solve to optimality with existing technologies. One fundamental difficulty of the MinDFA problem is the size of the search space. Moreover, another fundamental drawback of these approaches is the encoding size. This paper develops novel compact encodings for Symmetry Breaking of SAT-based approaches to MinDFA. The proposed encodings are shown to perform comparably in practice with the most efficient, but also significantly larger, symmetry breaking encodings.

5. On Computing the Union of MUSes Carlos Mencia, Oliver Kullmann, Alexey Ignatiev, and Joao Marques-Silva 22nd International Conference on Theory and Applications of Satisfiability Testing (SAT 2019) Lecture Notes in Computer Science, vol. 11628, pp. 211–221, 2019 [Abs] [HTML] [PDF]

   This paper considers unsatisfiable CNF formulas and addresses the problem of computing the union of the clauses included in some minimally unsatisfiable subformula (MUS). The union of MUSes represents a useful notion in infeasibility analysis since it summarizes all the causes for the unsatisfiability of a given formula. The paper proposes a novel algorithm for this problem, developing a refined recursive enumeration of MUSes based on powerful pruning techniques. Experimental results indicate the practical suitability of the approach.

6. DRMaxSAT with MaxHS: First Contact Antonio Morgado, Alexey Ignatiev, Maria Luisa Bonet, Joao Marques-Silva, and Sam Buss 22nd International Conference on Theory and Applications of Satisfiability Testing (SAT 2019) Lecture Notes in Computer Science, vol. 11628, pp. 239–249, 2019 [Abs] [HTML] [PDF]

   The proof system of Dual-Rail MaxSAT (DRMaxSAT) was recently shown to be capable of efficiently refuting families of formulas that are well-known to be hard for resolution, concretely when the MaxSAT solving approach is either MaxSAT resolution or core-guided algorithms. Moreover, DRMaxSAT based on MaxSAT resolution was shown to be stronger than general resolution. Nevertheless, existing experimental evidence indicates that the use of MaxSAT algorithms based on the computation of minimum hitting sets (MHSes), i.e. MaxHS-like algorithms, are as effective, and often more effective, than core-guided algorithms and algorithms based on MaxSAT resolution. This paper investigates the use of MaxHS-like algorithms in the DRMaxSAT proof system. Concretely, the paper proves that the propositional encoding of the pigenonhole and doubled pigenonhole principles have polynomial time refutations when the DRMaxSAT proof system uses a MaxHS-like algorithm.

7. Assessing Heuristic Machine Learning Explanations with Model Counting Nina Narodytska, Aditya Shrotri, Kuldeep S. Meel, Alexey Ignatiev, and Joao Marques-Silva 22nd International Conference on Theory and Applications of Satisfiability Testing (SAT 2019) Lecture Notes in Computer Science, vol. 11628, pp. 267–278, 2019 [Abs] [HTML] [PDF]

   Machine Learning (ML) models are widely used in decision making procedures in finance, medicine, education, etc. In these areas, ML outcomes can directly affect humans, e.g. by deciding whether a person should get a loan or be released from prison. Therefore, we cannot blindly rely on black box ML models and need to explain the decisions made by them. This motivated the development of a variety of ML-explainer systems, including LIME and its successor ANCHOR. Due to the heuristic nature of explanations produced by existing tools, it is necessary to validate them. We propose a SAT-based method to assess the quality of explanations produced by ANCHOR. We encode a trained ML model and an explanation for a given prediction as a propositional formula. Then, by using a state-of-the-art approximate model counter, we estimate the quality of the provided explanation as the number of solutions supporting it.

8. On Validating, Repairing and Refining Heuristic ML Explanations Alexey Ignatiev, Nina Narodytska, and Joao Marques-Silva CoRR abs/1907.02509, 2019 [Abs] [HTML] [Code]

   Recent years have witnessed a fast-growing interest in computing explanations for Machine Learning (ML) models predictions. For non-interpretable ML models, the most commonly used approaches for computing explanations are heuristic in nature. In contrast, recent work proposed rigorous approaches for computing explanations, which hold for a given ML model and prediction over the entire instance space. This paper extends earlier work to the case of boosted trees and assesses the quality of explanations obtained with state-of-the-art heuristic approaches. On most of the datasets considered, and for the vast majority of instances, the explanations obtained with heuristic approaches are shown to be inadequate when the entire instance space is (implicitly) considered.

9. On Relating Explanations and Adversarial Examples Alexey Ignatiev, Nina Narodytska, and Joao Marques-Silva 33rd Conference on Neural Information Processing Systems (NeurIPS 2019), pp. 15857–15867, 2019 [Abs] [HTML] [PDF] [Poster] [Code]

   The importance of explanations (XP’s) of machine learning (ML) model predictions and of adversarial examples (AE’s) cannot be overstated, with both arguably being essential for the practical success of ML in different settings. There has been recent work on understanding and assessing the relationship between XP’s and AE’s. However, such work has been mostly experimental and a sound theoretical relationship has been elusive. This paper demonstrates that explanations and adversarial examples are related by a generalized form of hitting set duality, which extends earlier work on hitting set duality observed in model-based diagnosis and knowledge compilation. Furthermore, the paper proposes algorithms, which enable computing adversarial examples from explanations and vice-versa.

2018

1. MaxSAT Resolution With the Dual Rail Encoding Maria Luisa Bonet, Sam Buss, Alexey Ignatiev, Joao Marques-Silva, and Antonio Morgado 32nd AAAI Conference on Artificial Intelligence (AAAI 2018), pp. 6565–6572, 2018 [Abs] [HTML] [PDF]

   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.

2. On Cryptographic Attacks Using Backdoors for SAT A. Semenov, O. Zaikin, I. Otpuschennikov, S. Kochemazov, and A. Ignatiev 32nd AAAI Conference on Artificial Intelligence (AAAI 2018), pp. 6641–6648, 2018 [Abs] [arXiv] [HTML] [PDF]

   Propositional satisfiability (SAT) is at the nucleus of state-of-the-art approaches to a variety of computationally hard problems, one of which is cryptanalysis. Moreover, a number of practical applications of SAT can only be tackled efficiently by identifying and exploiting a subset of formula’s variables called backdoor set (or simply backdoors). This paper proposes a new class of backdoor sets for SAT used in the context of cryptographic attacks, namely guess-and-determine attacks. The idea is to identify the best set of backdoor variables subject to a statistically estimated hardness of the guess-and-determine attack using a SAT solver. Experimental results on weakened variants of the renowned encryption algorithms exhibit advantage of the proposed approach compared to the state of the art in terms of the estimated hardness of the resulting guess-and-determine attacks.

3. A SAT-Based Approach to Learn Explainable Decision Sets Alexey Ignatiev, Filipe Pereira, Nina Narodytska, and Joao Marques-Silva 9th International Joint Conference on Automated Reasoning (IJCAR 2018) Lecture Notes in Computer Science, vol. 10900, pp. 627–645, 2018 [Abs] [HTML] [PDF]

   The successes of machine learning in recent years have triggered a fast growing range of applications. In important settings, including safety critical applications and when transparency of decisions is paramount, accurate predictions do not suffice; one expects the machine learning model to also explain the predictions made, in forms understandable by human decision makers. Recent work proposed explainable models based on decision sets which can be viewed as unordered sets of rules, respecting some sort of rule non-overlap constraint. This paper investigates existing solutions for computing decision sets and identifies a number of drawbacks, related with rule overlap and succinctness of explanations, the accuracy of achieved results, but also the efficiency of proposed approaches. To address these drawbacks, the paper develops novel SAT-based solutions for learning decision sets. Experimental results on computing decision sets for representative datasets demonstrate that SAT enables solutions that are not only the most efficient, but also offer stronger guarantees in terms of rule non-overlap.

4. Learning Optimal Decision Trees with SAT Nina Narodytska, Alexey Ignatiev, Filipe Pereira, and Joao Marques-Silva 27th International Joint Conference on Artificial Intelligence (IJCAI 2018), pp. 1362–1368, 2018 [Abs] [HTML] [PDF]

   Explanations of machine learning (ML) predictions are of fundamental importance in different settings. Moreover, explanations should be succinct, to enable easy understanding by humans. Decision trees represent an often used approach for developing explainable ML models, motivated by the natural mapping between decision tree paths and rules. Clearly, smaller trees correlate well with smaller rules, and so one challenge is to devise solutions for computing smallest size decision trees given training data. Although simple to formulate, the computation of smallest size decision trees turns out to be an extremely challenging computational problem, for which no practical solutions are known. This paper develops a SAT-based model for computing smallest-size decision trees given training data. In sharp contrast with past work, the proposed SAT model is shown to scale for publicly available datasets of practical interest.

5. PySAT: A Python Toolkit for Prototyping with SAT Oracles Alexey Ignatiev, Antonio Morgado, and Joao Marques-Silva 21st International Conference on Theory and Applications of Satisfiability Testing (SAT 2018) Lecture Notes in Computer Science, vol. 10929, pp. 428–437, 2018 [Abs] [HTML] [PDF] [Code]

   Boolean satisfiability (SAT) solvers are at the core of efficient approaches for solving a vast multitude of practical problems. Moreover, albeit targeting an NP-complete problem, SAT solvers are increasingly used for tackling problems beyond NP. Despite the success of SAT in practice, modeling with SAT and more importantly implementing SAT-based problem solving solutions is often a difficult and error-prone task. This paper proposes the PySAT toolkit, which enables fast Python-based prototyping using SAT oracles and SAT-related technology. PySAT provides a simple API for working with a few state-of-the-art SAT oracles and also integrates a number of cardinality constraint encodings, all aiming at simplifying the prototyping process. Experimental results presented in the paper show that PySAT-based implementations can be as efficient as those written in a low-level language.

2017

1. Debugging EL+ Ontologies through Horn MUS Enumeration Alexey Ignatiev, Joao Marques-Silva, Carlos Mencia, and Rafael Peñaloza 30th International Workshop on Description Logics (DL 2017) CEUR Workshop Proceedings, vol. 1879, 2017 [Abs] [HTML] [PDF]

   In description logics (DLs), axiom pinpointing refers to the problem of enumerating the minimal subsets of axioms from an ontology that entail a given consequence. Recent developments on axiom pinpointing for the light-weight DL EL+ are based on translating this problem into the enumeration of all minimally unsatisfiable subformulas (MUSes)of a propositional formula, and using advanced SAT-based techniques for solving it. Further optimizations have been obtained by targeting the MUS enumerator to the specific properties of the formula obtained. In this paper we describe different improvements that have been considered since the translation was first proposed. Through an empirical study, we analyse the behaviour of these techniques and how it depends on different characteristics of the original pinpointing problem, and the translated SAT formula.

2. Horn Maximum Satisfiability: Reductions, Algorithms and Applications Joao Marques-Silva, Alexey Ignatiev, and Antonio Morgado 18th EPIA Conference on Artificial Intelligence (EPIA 2017) Lecture Notes in Computer Science, vol. 10423, pp. 681–694, 2017 [Abs] [arXiv] [HTML] [PDF]

   Recent years have witnessed remarkable performance improvements in maximum satisfiability (MaxSAT) solvers. In practice, MaxSAT algorithms often target the most generic MaxSAT formulation, whereas dedicated solvers, which address specific subclasses of MaxSAT, have not been investigated. This paper shows that a wide range of optimization and decision problems are either naturally formulated as MaxSAT over Horn formulas, or permit simple encodings using HornMaxSAT. Furthermore, the paper also shows how linear time decision procedures for Horn formulas can be used for developing novel algorithms for the HornMaxSAT problem.

3. Lean Kernels in Description Logics Rafael Peñaloza, Carlos Mencia, Alexey Ignatiev, and Joao Marques-Silva 14th European Semantic Web Conference (ESWC 2017) Lecture Notes in Computer Science, vol. 10249, pp. 518–533, 2017 [Abs] [HTML] [PDF]

   Lean kernels (LKs) are an effective optimization for deriving the causes of unsatisfiability of a propositional formula. Interestingly, no analogous notion exists for explaining consequences of description logic (DL) ontologies. We introduce LKs for DLs using a general notion of consequence-based methods, and provide an algorithm for computing them which incurs in only a linear time overhead. As an example, we instantiate our framework to the DL ALC. We prove formally and empirically that LKs provide a tighter approximation of the set of relevant axioms for a consequence than syntactic locality-based modules.

4. On Computing Generalized Backbones Alessandro Previti, Alexey Ignatiev, Matti Järvisalo, and Joao Marques-Silva 29th International Conference on Tools with Artificial Intelligence (ICTAI 2017), pp. 1050–1056, 2017 [Abs] [HTML] [PDF]

   The concept of backbone variables, i.e., variables that take the same value in all solutions-or, equivalently, never take a specific value-finds various important applications in the context of Boolean satisfiability (SAT), motivating the development of efficient algorithms for determining the set of backbone variables of a given propositional formula. Notably, this problem surpasses the complexity of merely deciding satisfiability. In this work we consider generalizations of the concept of backbones in SAT to non-binary (and potentially infinite) domain constraint satisfaction problems. Specifically, we propose a natural generalization of backbones to the context of satisfiability modulo theories (SMT), applicable to a range of different theories as well as CSPs in general, and provide two generic algorithms for determining the backbone in this general context. As two concrete instantiations, we focus on two central SMT theories, the theory of linear integer arithmetic (LIA) with infinite integer domains, and the theory of bit vectors (BV), and empirically evaluate the potential of the proposed algorithms on both LIA and BV instances.

5. Cardinality Encodings for Graph Optimization Problems Alexey Ignatiev, Antonio Morgado, and Joao Marques-Silva 26th International Joint Conference on Artificial Intelligence (IJCAI 2017), pp. 652–658, 2017 [Abs] [HTML] [PDF] [Slides]

   Different optimization problems defined on graphs find application in complex network analysis. Existing propositional encodings render impractical the use of propositional satisfiability (SAT) and maximum satisfiability (MaxSAT) solvers for solving a variety of these problems on large graphs. This paper has two main contributions. First, the paper identifies sources of inefficiency in existing encodings for different optimization problems in graphs. Second, for the concrete case of the maximum clique problem, the paper develops a novel encoding which is shown to be far more compact than existing encodings for large sparse graphs. More importantly, the experimental results show that the proposed encoding enables existing SAT solvers to compute a maximum clique for large sparse networks, often more efficiently than the state of the art.

6. On Tackling the Limits of Resolution in SAT Solving Alexey Ignatiev, Antonio Morgado, and Joao Marques-Silva 20th International Conference on Theory and Applications of Satisfiability Testing (SAT 2017) Lecture Notes in Computer Science, vol. 10491, pp. 164–183, 2017 [Abs] [arXiv] [HTML] [PDF] [Slides]

   The practical success of Boolean Satisfiability (SAT) solvers stems from the CDCL (Conflict-Driven Clause Learning) approach to SAT solving. However, from a propositional proof complexity perspective, CDCL is no more powerful than the resolution proof system, for which many hard examples exist. This paper proposes a new problem transformation, which enables reducing the decision problem for formulas in conjunctive normal form (CNF) to the problem of solving maximum satisfiability over Horn formulas. Given the new transformation, the paper proves a polynomial bound on the number of MaxSAT resolution steps for pigeonhole formulas. This result is in clear contrast with earlier results on the length of proofs of MaxSAT resolution for pigeonhole formulas. The paper also establishes the same polynomial bound in the case of modern core-guided MaxSAT solvers. Experimental results, obtained on CNF formulas known to be hard for CDCL SAT solvers, show that these can be efficiently solved with modern MaxSAT solvers.

2016

1. BEACON: An Efficient SAT-Based Tool for Debugging EL+ Ontologies M. F. Arif, C. Mencia, A. Ignatiev, N. Manthey, R. Peñaloza, and J. Marques-Silva 19th International Conference on Theory and Applications of Satisfiability Testing (SAT 2016) Lecture Notes in Computer Science, vol. 9710, pp. 521–530, 2016 [Abs] [HTML] [PDF]

   Description Logics (DLs) are knowledge representation and reasoning formalisms used in many settings. Among them, the EL family of DLs stands out due to the availability of polynomial-time inference algorithms and its ability to represent knowledge from domains such as medical informatics. However, the construction of an ontology is an error-prone process which often leads to unintended inferences. This paper presents the BEACON tool for debugging EL+ ontologies. BEACON builds on earlier work relating minimal justifications (MinAs) of EL+ ontologies and MUSes of a Horn formula, and integrates state-of-the-art algorithms for solving different function problems in the SAT domain.

2. Quantified maximum satisfiability Alexey Ignatiev, Mikolas Janota, and Joao Marques-Silva Constraints, vol. 21(2), pp. 277–302, 2016 [Abs] [HTML] [PDF]

   In recent years, there have been significant improvements in algorithms both for Quantified Boolean Formulas (QBF) and for Maximum Satisfiability (MaxSAT). This paper studies an optimization extension of QBF and considers the problem in a quantified MaxSAT setting. More precisely, the general QMaxSAT problem is defined for QBFs with a set of soft clausal constraints and consists in finding the largest subset of the soft constraints such that the remaining QBF is true. Two approaches are investigated. One is based on relaxing the soft clauses and performing an iterative search on the cost function. The other approach, which is the main contribution of the paper, is inspired by recent work on MaxSAT, and exploits the iterative identification of unsatisfiable cores. The paper investigates the application of these approaches to the two concrete problems of computing smallest minimal unsatisfiable subformulas (SMUS) and smallest minimal equivalent subformulas (SMES), decision versions of which are well-known problems in the second level of the polynomial hierarchy. Experimental results, obtained on representative problem instances, indicate that the core-guided approach for the SMUS and SMES problems outperforms the use of iterative search over the values of the cost function. More significantly, the core-guided approach to SMUS also outperforms the state-of-the-art SMUS extractor Digger.

3. On Finding Minimum Satisfying Assignments Alexey Ignatiev, Alessandro Previti, and Joao Marques-Silva 22nd International Conference on Principles and Practice of Constraint Programming (CP 2016) Lecture Notes in Computer Science, vol. 9892, pp. 287–297, 2016 [Abs] [HTML] [PDF] [Slides]

   Given a Satisfiability Modulo Theories (SMT) formula, a minimum satisfying assignment (MSA) is a partial assignment of minimum size that ensures the formula is satisfied. Minimum satisfying assignments find a number of practical applications that include software and hardware verification, among others. Recent work proposes the use of branch-and-bound search for computing MSAs. This paper proposes a novel counterexample-guided implicit hitting set approach for computing one MSA. Experimental results show significant performance gains over existing approaches.

4. On Incremental Core-Guided MaxSAT Solving Xujie Si, Xin Zhang, Vasco Manquinho, Mikolas Janota, Alexey Ignatiev, and Mayur Naik 22nd International Conference on Principles and Practice of Constraint Programming (CP 2016) Lecture Notes in Computer Science, vol. 9892, pp. 473–482, 2016 [Abs] [HTML] [PDF] [Slides]

   This paper aims to improve the efficiency of unsat core-guided MaxSAT solving on a sequence of similar problem instances. In particular, we consider the case when the sequence is constructed by adding new hard or soft clauses. Our approach is akin to the well-known idea of incremental SAT solving. However, we show that there are important differences between incremental SAT and incremental MaxSAT, where a straightforward implementation may lead to a sharp decrease in performance. We present alternatives that enable to cope with such issues. The presented algorithm is implemented and evaluated on practical problems. It solves more instances and yields an average speedup of 1.8× on previously solvable instances.

5. Propositional Abduction with Implicit Hitting Sets Alexey Ignatiev, Antonio Morgado, and Joao Marques-Silva 22nd European Conference on Artificial Intelligence (ECAI 2016) Frontiers in Artificial Intelligence and Applications, vol. 285, pp. 1327–1335, 2016 [Abs] [arXiv] [HTML] [PDF]

   Logic-based abduction finds important applications in artificial intelligence and related areas. One application example is in finding explanations for observed phenomena. Propositional abduction is a restriction of abduction to the propositional domain, and complexity-wise is in the second level of the polynomial hierarchy. Recent work has shown that exploiting implicit hitting sets and propositional satisfiability (SAT) solvers provides an efficient approach for propositional abduction. This paper investigates this earlier work and proposes a number of algorithmic improvements. These improvements are shown to yield exponential reductions in the number of SAT solver calls. More importantly, the experimental results show significant performance improvements compared to the the best approaches for propositional abduction.

6. Efficient Reasoning for Inconsistent Horn Formulae Joao Marques-Silva, Alexey Ignatiev, Carlos Mencia, and Rafael Peñaloza 15th European Conference On Logics In Artificial Intelligence (JELIA 2016) Lecture Notes in Computer Science, vol. 10021, pp. 336–352, 2016 [Abs] [HTML] [PDF]

   Horn formulae are widely used in different settings that include logic programming, answer set programming, description logics, deductive databases, and system verification, among many others. One concrete example is concept subsumption in lightweight description logics, which can be reduced to inference in propositional Horn formulae. Some problems require one to reason with inconsistent Horn formulae. This is the case when providing minimal explanations of inconsistency. This paper proposes efficient algorithms for a number of decision, function and enumeration problems related with inconsistent Horn formulae. Concretely, the paper develops efficient algorithms for finding and enumerating minimal unsatisfiable subsets (MUSes), minimal correction subsets (MCSes), but also for computing the lean kernel. The paper also shows the practical importance of some of the proposed algorithms.

7. MCS Extraction with Sublinear Oracle Queries Carlos Mencia, Alexey Ignatiev, Alessandro Previti, and Joao Marques-Silva 19th International Conference on Theory and Applications of Satisfiability Testing (SAT 2016) Lecture Notes in Computer Science, vol. 9710, pp. 342–360, 2016 [Abs] [HTML] [PDF]

   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.

8. Maximal falsifiability Alexey Ignatiev, Antonio Morgado, Jordi Planes, and Joao Marques-Silva AI Commun., vol. 29(2), pp. 351–370, 2016 [Abs] [HTML] [PDF]

   Similarly to Maximum Satisfiability (MaxSAT), Minimum Satisfiability (MinSAT) is an optimization extension of the Boolean Satisfiability (SAT) decision problem. In recent years, both problems have been studied in terms of exact and approximation algorithms. In addition, the MaxSAT problem has been characterized in terms of Maximal Satisfiable Subsets (MSSes) and Minimal Correction Subsets (MCSes), as well as Minimal Unsatisfiable Subsets (MUSes) and minimal hitting set dualization. However, and in contrast with MaxSAT, no such characterizations exist for MinSAT. This paper addresses this issue by casting the MinSAT problem in a more general framework. The paper studies Maximal Falsifiability, the problem of computing a subset-maximal set of clauses that can be simultaneously falsified, and shows that MinSAT corresponds to the complement of a largest subset-maximal set of simultaneously falsifiable clauses, i.e. the solution of the Maximum Falsifiability (MaxFalse) problem. Additional contributions of the paper include novel algorithms for Maximum and Maximal Falsifiability, as well as minimal hitting set dualization results for the MaxFalse problem. Moreover, the proposed algorithms are validated on practical instances.

2015

1. Smallest MUS Extraction with Minimal Hitting Set Dualization Alexey Ignatiev, Alessandro Previti, Mark H. Liffiton, and Joao Marques-Silva 21st International Conference on Principles and Practice of Constraint Programming (CP 2015) Lecture Notes in Computer Science, vol. 9255, pp. 173–182, 2015 [Abs] [HTML] [PDF]

   Minimal explanations of infeasibility are of great interest in many domains. In propositional logic, these are referred to as Minimal Unsatisfiable Subsets (MUSes). An unsatisfiable formula can have multiple MUSes, some of which provide more insights than others. Different criteria can be considered in order to identify a good minimal explanation. Among these, the size of an MUS is arguably one of the most intuitive. Moreover, computing the smallest MUS (SMUS) finds several practical applications that include validating the quality of the MUSes computed by MUS extractors and finding equivalent subformulae of smallest size, among others. This paper develops a novel algorithm for computing a smallest MUS, and we show that it outperforms all the previous alternatives pushing the state of the art in SMUS solving. Although described in the context of propositional logic, the presented technique can also be applied to other constraint systems.

2. Efficient Model Based Diagnosis with Maximum Satisfiability Joao Marques-Silva, Mikolas Janota, Alexey Ignatiev, and Antonio Morgado 24th International Joint Conference on Artificial Intelligence (IJCAI 2015), pp. 1966–1972, 2015 [Abs] [HTML] [PDF] [Slides]

   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.

3. Prime Compilation of Non-Clausal Formulae Alessandro Previti, Alexey Ignatiev, Antonio Morgado, and Joao Marques-Silva 24th International Joint Conference on Artificial Intelligence (IJCAI 2015), pp. 1980–1988, 2015 [Abs] [HTML] [PDF]

   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.

4. SAT-Based Formula Simplification Alexey Ignatiev, Alessandro Previti, and Joao Marques-Silva 18th International Conference on Theory and Applications of Satisfiability Testing (SAT 2015) Lecture Notes in Computer Science, vol. 9340, pp. 287–298, 2015 [Abs] [HTML] [PDF]

   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.

2014

1. MSCG: Robust Core-Guided MaxSAT Solving Antonio Morgado, Alexey Ignatiev, and Joao Marques-Silva Journal on Satisfiability, Boolean Modeling and Computation, vol. 9, pp. 129–134, 2014 [Abs] [HTML] [PDF]

   Maximum Satisfiability (MaxSAT) is a well-known optimization version of Propositional Satisfiability (SAT) that finds a wide range of relevant practical applications. This work describes and evaluates the Maximum Satisfiability using the Core-Guided approach solver (MSCG), which is a robust MaxSAT solver that participated in the MaxSAT Evaluation 2014. An experimental comparison with state-of-the-art MaxSAT solvers is presented.

2. Progression in Maximum Satisfiability Alexey Ignatiev, Antonio Morgado, Vasco Manquinho, Inês Lynce, and Joao Marques-Silva 21st European Conference on Artificial Intelligence (ECAI 2014) Frontiers in Artificial Intelligence and Applications, vol. 263, pp. 453–458, 2014 [Abs] [HTML] [PDF]

   Maximum Satisfiability (MaxSAT) is a well-known optimization version of Propositional Satisfiability (SAT), that finds a wide range of relevant practical applications. Despite the significant progress made in MaxSAT solving in recent years, many practically relevant problem instances require prohibitively large run times, and many cannot simply be solved with existing algorithms. One approach for solving MaxSAT is based on iterative SAT solving, which may optionally be guided by unsatisfiable cores. A difficulty with this class of algorithms is the possibly large number of times a SAT solver is called, e.g. for instances with very large clause weights. This paper proposes the use of geometric progressions to tackle this issue, thus allowing, for the vast majority of problem instances, to reduce the number of calls to the SAT solver. The new approach is also shown to be applicable to core-guided MaxSAT algorithms. Experimental results, obtained on a large number of problem instances, show gains when compared to state-of-the-art implementations of MaxSAT algorithms.

3. Efficient Autarkies Joao Marques-Silva, Alexey Ignatiev, Antonio Morgado, Vasco Manquinho, and Inês Lynce 21st European Conference on Artificial Intelligence (ECAI 2014) Frontiers in Artificial Intelligence and Applications, vol. 263, pp. 603–608, 2014 [Abs] [HTML] [PDF]

   Autarkies are partial truth assignments that satisfy all clauses having literals in the assigned variables. Autarkies provide important information in the analysis of unsatisfiable formulas. Indeed, clauses satisfied by autarkies cannot be included in minimal explanations or in minimal corrections of unsatisfiability. Computing the maximum autarky allows identifying all such clauses. In recent years, a number of alternative approaches have been proposed for computing a maximum autarky. This paper develops new models for representing autarkies, and proposes new algorithms for computing the maximum autarky. Experimental results, obtained on a large number of problem instances, show orders of magnitude performance improvements over existing approaches, and solving instances that could not otherwise be solved.

4. Towards efficient optimization in package management systems Alexey Ignatiev, Mikolas Janota, and Joao Marques-Silva 36th International Conference on Software Engineering (ICSE 2014), pp. 745–755, 2014 [Abs] [HTML] [PDF] [Slides]

   Package management as a means of reuse of software artifacts has become extremely popular, most notably in Linux distributions. At the same time, successful package management brings about a number of computational challenges. Whenever a user requires a new package to be installed, a package manager not only installs the new package but it might also install other packages or uninstall some old ones in order to respect dependencies and conflicts of the packages. Coming up with a new configuration of packages is computationally challenging. It is in particular complex when we also wish to optimize for user preferences, such as that the resulting package configuration should not differ too much from the original one. A number of exact approaches for solving this problem have been proposed in recent years. These approaches, however, do not have guaranteed runtime due to the high computational complexity of the problem. This paper addresses this issue by devising a hybrid approach that integrates exact solving with approximate solving by invoking the approximate part whenever the solver is running out of time. Experimental evaluation shows that this approach enables returning high-quality package configurations with rapid response time.

5. On Reducing Maximum Independent Set to Minimum Satisfiability Alexey Ignatiev, Antonio Morgado, and Joao Marques-Silva 17th International Conference on Theory and Applications of Satisfiability Testing (SAT 2014) Lecture Notes in Computer Science, vol. 8561, pp. 103–120, 2014 [Abs] [HTML] [PDF] [Slides]

   Maximum Independent Set (MIS) is a well-known NP-hard graph problem, tightly related with other well known NP-hard graph problems, namely Minimum Vertex Cover (MVC) and Maximum Clique (MaxClq). This paper introduces a novel reduction of MIS into Minimum Satisfiability (MinSAT), thus, providing an alternative approach for solving MIS. The reduction naturally maps the vertices of a graph into clauses, without requiring the inclusion of hard clauses. Moreover, it is shown that the proposed reduction uses fewer variables and clauses than the existing alternative of mapping MIS into Maximum Satisfiability (MaxSAT). The paper develops a number of optimizations to the basic reduction, which significantly reduce the total number of variables used. The experimental evaluation considered the reductions described in the paper as well as existing state-of-the-art approaches. The results show that the proposed approaches based on MinSAT are competitive with existing approaches.

2013

1. Maximal Falsifiability: Definitions, Algorithms, and Applications Alexey Ignatiev, Antonio Morgado, Jordi Planes, and Joao Marques-Silva 19th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR 2013) Lecture Notes in Computer Science, vol. 8312, pp. 439–456, 2013 [Abs] [HTML] [PDF] [Slides]

   Similarly to Maximum Satisfiability (MaxSAT), Minimum Satisfiability (MinSAT) is an optimization extension of the Boolean Satisfiability (SAT) decision problem. In recent years, both problems have been studied in terms of exact and approximation algorithms. In addition, the MaxSAT problem has been characterized in terms ofMaximal Satisfiable Subsets (MSSes) andMinimal Correction Subsets (MCSes), as well as Minimal Unsatisfiable Subsets (MUSes) and minimal hitting set dualization. However, and in contrast with MaxSAT, no such characterizations exist for MinSAT. This paper addresses this issue by casting the MinSAT problem in a more general framework. The paper studies Maximal Falsifiability, the problem of computing a subset-maximal set of clauses that can be simultaneously falsified, and shows that MinSAT corresponds to the complement of a largest subset-maximal set of simultaneously falsifiable clauses, i.e. the solution of the Maximum Falsifiability (MaxFalse) problem. Additional contributions of the paper include novel algorithms for Maximum and Maximal Falsifiability, as well as minimal hitting set dualization results for the MaxFalse problem. Moreover, the proposed algorithms are validated on practical instances.

2. Quantified Maximum Satisfiability: A Core-Guided Approach Alexey Ignatiev, Mikolas Janota, and Joao Marques-Silva 16th International Conference on Theory and Applications of Satisfiability Testing (SAT 2013) Lecture Notes in Computer Science, vol. 7962, pp. 250–266, 2013 [Abs] [HTML] [PDF] [Slides]

   In recent years, there have been significant improvements in algorithms both for Quantified Boolean Formulas (QBF) and for Maximum Satisfiability (MaxSAT). This paper studies the problem of solving quantified formulas subject to a cost function, and considers the problem in a quantified MaxSAT setting. Two approaches are investigated. One is based on relaxing the soft clauses and performing a linear search on the cost function. The other approach, which is the main contribution of the paper, is inspired by recent work on MaxSAT, and exploits the iterative identification of unsatisfiable cores. The paper investigates the application of these approaches to the concrete problem of computing smallest minimal unsatisfiable subformulas (SMUS), a decision version of which is a well-known problem in the second level of the polynomial hierarchy. Experimental results, obtained on representative problem instances, indicate that the core-guided approach for the SMUS problem outperforms the use of linear search over the values of the cost function. More significantly, the core-guided approach also outperforms the state-of-the-art SMUS extractor Digger.

2011

1. DPLL+ROBDD Derivation Applied to Inversion of Some Cryptographic Functions Alexey Ignatiev and Alexander A. Semenov 14th International Conference on Theory and Applications of Satisfiability Testing (SAT 2011) Lecture Notes in Computer Science, vol. 6695, pp. 76–89, 2011 [Abs] [HTML] [PDF] [Slides]

   The paper presents logical derivation algorithms that can be applied to inversion of polynomially computable discrete functions. The proposed approach is based on the fact that it is possible to organize DPLL derivation on a small subset of variables appeared in a CNF which encodes the algorithm computing the function. The experimental results showed that arrays of conflict clauses generated by this mode of derivation, as a rule, have efficient ROBDD representations. This fact is the departing point of development of a hybrid DPLL+ROBDD derivation strategy: derivation techniques for ROBDD representations of conflict databases are the same as those ones in common DPLL (variable assignments and unit propagation). In addition, compact ROBDD representations of the conflict databases can be shared effectively in a distributed computing environment.