Explainability via Short Formulas: the Case of Propositional Logic with Implementation

Abstract

We conceptualize explainability in terms of logic and formula size, giving a number of related definitions of explainability in a very general setting. Our main interest is the so-called local explanation problem which aims to explain the truth value of an input formula in an input model. The explanation is a formula of minimal size that (1) obtains the same truth value as the input formula on the input model and (2) transmits that truth value to the input formula globally, i.e., on every model. As an important example case, we study propositional logic in this setting and show that the local explainability problem is complete for the second level of the polynomial hierarchy. The hardness result holds already for DNF-formulas. We also give parameterized versions of these problems leading to NP-completeness. The generality of our definitions allows us to lift complexity results also, e.g., to S5 modal logic and ensembles of decision trees. We also provide an implementation in answer set programming and investigate its capacity in relation to explaining answers to the n-queens and dominating set problems. Furthermore, we give an example of explaining the behavior of a black-box classifier.