=Paper=
{{Paper
|id=Vol-3281/paper6
|storemode=property
|title=Explainability via Short Formulas: the Case of Propositional Logic with Implementation
|pdfUrl=https://ceur-ws.org/Vol-3281/paper6.pdf
|volume=Vol-3281
|authors=Reijo Jaakkola,Tomi Janhunen,Antti Kuusisto,Masood Feyzbakhsh Rankooh,Miikka Vilander
|dblpUrl=https://dblp.org/rec/conf/lpnmr/JaakkolaJKRV22
}}
==Explainability via Short Formulas: the Case of Propositional Logic with Implementation==
https://ceur-ws.org/Vol-3281/paper6.pdf
Explainability via Short Formulas: the Case of
Propositional Logic with Implementation
Reijo Jaakkola1 , Tomi Janhunen2 , Antti Kuusisto3 , Masood Feyzbakhsh Rankooh4 and
Miikka Vilander5,β
Tampere University, FI-33014, Tampere University, Finland
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 special 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) agrees with the input formula on the input model and (2) transmits the involved
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 special explainability problem is complete for the
second level of the polynomial hierarchy. We also provide an implementation of this problem in answer
set programming and investigate its capacity in relation to explaining answers to the n-queens and
dominating set problems.
Keywords
explainability, answer set programming, satisfiability checking, computational complexity
1. Introduction
This paper investigates explainability in a general setting. The key in our approach is to relate
explainability to formula size. We differentiate between the general and special explanation
problems. The general explanation problem for a logic L takes as input a formula π β L and
outputs an equivalent formula of minimal size. Thus the objective is to explain the global
behavior of π. For example, we can consider ¬¬¬¬¬¬π to be globally explained by π. In
contrast, the goal of the special explanation problem is to explicate why an input formula π gets
the truth value π in an input model π. Given a tuple (π, π , π), the problem outputs a formula π
of minimal size such that (1) the formula π obtains the same truth value π on π, and (2) on every
model π β² where π gets the truth value π, also π gets that same truth value. Intuitively, this
second condition states that the given truth value π of π on a model π β² causes π to be judged
similarly. In summary, the special explanation problem gives reasons why a piece of data (or a
Accepted for presentation at the 29th RCRA Workshop, 2022, Genoa, Italy
β
Corresponding author.
Envelope-Open reijo.jaakkola@tuni.fi (R. Jaakkola); tomi.janhunen@tuni.fi (T. Janhunen); antti.kuusisto@tuni.fi (A. Kuusisto);
masood.feyzbakhshrankooh@tuni.fi (M. F. Rankooh); miikka.vilander@tuni.fi (M. Vilander)
GLOBE https://reijojaakkola.github.io/ (R. Jaakkola); https://tuni.fi/en/tomi-janhunen (T. Janhunen);
https://homepages.tuni.fi/antti.kuusisto/ (A. Kuusisto)
Orcid 0000-0003-4714-4637 (R. Jaakkola); 0000-0002-2029-7708 (T. Janhunen); 0000-0003-1356-8749 (A. Kuusisto);
0000-0001-5660-3052 (M. F. Rankooh); 0000-0002-7301-939X (M. Vilander)
Β© 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
Workshop
Proceedings
http://ceur-ws.org
ISSN 1613-0073
CEUR Workshop Proceedings (CEUR-WS.org)
model) is treated in a given way (i.e., obtains a given truth value) by a classifier (or a formula).
The two explanation problems give rise to corresponding questions of explainability. The
general explainability problem for a logic L asks, given a formula π β L and π β β, whether
there exists a formula equivalent to π of size at most π. The special explainability problem gets
as input a tuple (π, π , π, π), and the task is then to check whether there exists a formula π of
size at most π satisfying the above conditions (1) and (2) of the special explanation problem.
As an important particular case, we study the special explainability problem of propositional
logic (PL) in detail. We prove that the problem is Ξ£π2 -complete. This is an important result
whose usefulness lies in its implications that go far beyond PL itself. Indeed, the result gives a
robust lower bound for various logics. We demonstrate this by establishing Ξ£π2 -completeness of
the special explainability problem of S5 modal logic; the lower bound follows directly from the
case of PL, while the upper bound is very easy to obtain. We observe that a rather wide range
of logics with satisfiability in NP have Ξ£π2 -complete special explainability problems.
As a further theoretical result, we prove that, when limiting to explaining only the positive
truth value β€, the special explainability problem is only NP-complete for CNF -formulas of PL.
As a corollary, we get NP-completeness of the problem for DNF -formulas in restriction to the
truth value β₯. While theoretically interesting, these results are also relevant from the point of
view of applications, as quite often real-life classification scenarios require explanations only
in the case of one truth value. For example, explanations concerning automated insurance
decisions are typically relevant only in the case of rejected applications. In addition to the
NP-completeness results, we also show that restricting to a single truth value here is necessary
for obtaining the given complexity (supposing coNP β NP).
We provide an implementation of the special explainability problem of PL based on answer-set
programming (ASP) [1]. Generally, ASP is a logic programming language based on stable-
model semantics and propositional syntax, particularly Horn clauses. ASP is especially suitable
and almost custom-made for implementing the special explainability problem of PL, as ASP
is designed precisely for the complexity levels up to Ξ£π2 . Indeed, while the disjunction-free
fragments of ASP [2] cover the first level of the polynomial hierarchy in a natural way, proper
disjunctive rules with cyclic dependencies become necessary to reach the second one [3].
We test the implementation via experiments with benchmarks based on the π-queens and
dominating set problems. The experiments provide concrete and compact explanations why a
particular configuration of queens on the generalized chessboard or a particular set of vertices of
a graph is or is not an acceptable solution to the involved problem. Runtimes scale exponentially
in the size of the instance and negative explanations tend to be harder to compute than positive
ones. Also, we observe from the experiments that the respective optimization variants of
explanations problems can be computationally more effective, leaving the exact bound on the
size of explaining formulas open and relieving the user from providing a particular bound.
Concerning related work, while the literature on explainability is extensive, only a small
part of it is primarily based on logic. In relation to the current paper, the special explainability
problem in the particular case of PL has some similarities with the prime implicant (or PI)
explanations of [4]. However, there are some key differences. PI-explanations are defined in
terms of finding a minimal subset of featuresβor propositionsβthat suffice to explain the input
instance of a Boolean decision function. Our definition of special explainability allows for any
kind of formula as output. In the propositional case, we separately prove that a subconjunction
of the literals in the input is always a possible output. We end up with a similar goal of removing
propositions, but from a different starting point and in a different setting. In the case of other
logics, such as FO, the resemblance to prime implicant explanations decreases. Concerning
results, [4] does not provide a full complexity analysis relating to the studied problems. Although
PI-explanations are defined for any decision function, the algorithms used in [4] to compute
PI-explanations have ordered binary decision diagrams (OBDD) as inputs and outputs. For these
algorithms, the authors give empirical runtimes but no complexity bounds. Thus, in our work,
while the space of potential input and output formulas is different, we also give a complete
complexity analysis of the special explainability problem in addition to experiments.
π
In [5], Umans shows that the shortest implicant problem is Ξ£2 -complete, thereby solving a
long-standing open problem of Stockmeyer. An implicant of π is a conjunction π of literals such
that π β¨ π. The shortest implicant problem asks whether there is an implicant of π with size
at most π. Size is defined as the number of occurrences of literals. Below we prove that the
special explainability problem for PL can be reduced to certain particular implicant problems.
π
However, despite this, the work of Umans does not directly modify to give the Ξ£2 -completeness
result of the special explainability problem. The key issue is that the explainability problem
requires an interpolant between a set π of literals and a formula π, where π has precisely the
same set of propositions symbols as π. Thus we need to give an independent proof for the Ξ£π2
lower bound. Also, formula size in [5] is measured in a more coarse way.
2. Preliminaries
Let Ξ¦ be a set of proposition symbols. The set PL(Ξ¦) of formulas of propositional logic PL
over Ξ¦ is given by the grammar π βΆ= π β£ Β¬π β£ (π β§ π) β£ (π β¨ π), where π β Ξ¦. Literals are either
atoms π or their negations Β¬π, also known as positive and negative literals, respectively. A
Ξ¦-assignment is a function π βΆ Ξ¦ β {0, 1}. When Ξ¦ is clear from the context or irrelevant, we
simply refer to assignments rather than Ξ¦-assignments. We define the semantics of propositional
logic in the usual way, and we write π β§ π if the assignment π satisfies the formula π β PL(Ξ¦).
Alternatively, we can use the standard valuation function π£Ξ¦ defined such that π£Ξ¦ (π , π) = 1 if
π β¨ π and otherwise π£Ξ¦ (π , π) = 0. Below we sometimes use the set {β₯, β€} instead of {0, 1},
A formula π β PL(Ξ¦) is a logical consequence of π β PL(Ξ¦), denoted π β¨ π, if for every
Ξ¦-assignment π , π β¨ π implies π β¨ π. A formula π β PL(Ξ¦) is an interpolant between π and π if
π β¨ π and π β¨ π. For a finite Ξ¦, we say that a formula π is a maximal conjunction w.r.t. Ξ¦ if π
is a conjunction of exactly one literal for each π β Ξ¦. A Ξ¦-assignment π can be naturally identified
with a maximal conjunction, for example {(π, 1), (π, 0)} identifies with π β§ Β¬π. A formula π is
a subconjunction of π if π is a conjunction of literals occurring in π. The size of π, denoted
size(π), is the number of occurrences of proposition symbols, binary connectives and negations
in π. For example, the size of ¬¬(π β§ π) is 5 as it has one β§ and two occurrences of both Β¬ and π.
3. Notions of explanation and explainability
In this section we introduce four natural problems concerning the general and special per-
spectives to explainability. The general problems deal with the question of explaining the
entire behavior of a classifier, whereas the special ones attempt to explicate why a single input
instance was classified in a given way. We give very general definitions of these problems, and
for that we will devise a very general definition of the notion of a logic. Our definition of a
logic covers various kinds of classifiers in addition to standard formal logics, including logic
programs, Turing machines, neural network models, automata, and the like.
Definition 1. A logic is a tuple (β³, β± , π£, π) where β³ and β± are sets; π£ βΆ β³ Γ β± β π is a
function mapping to some set π; and π βΆ β± β β is a function. Emphasizing the set π, we can
also call (β³, β± , π£, π) a π-valued logic.
Intuitively, we can think of β³ as a set of models and β± as a set of formulas. The function
π£ βΆ β³ Γ β± β π gives the semantics of the logic, with π£(π, π) being the truth value of π in π.
We call π£ a valuation. The function π gives a complexity measure for the formulas in β±, such
as, for example, formula size.
Example 2. Propositional logic PL over a set Ξ¦ of proposition symbols can be defined as a tuple
(β³, β± , π£, π), where β³ is the set of Ξ¦-assignments; β± the set PL(Ξ¦) of formulas; π£ βΆ β³ Γ β± β
{0, 1} is the standard valuation π£Ξ¦ ; and π(π) = size(π) for all π β β±.
Now, the following example demonstrates that we can consider much more general scenarios
than ones involving the standard formal logics.
Example 3. Let β³ be a set of data and β± a set of programs for classifying the data, that is,
programs that take elements of β³ as inputs and output a value in some set π of suitable outputs.
Now π£ βΆ β³ Γ β± β π is just the function such that π£(π·, π) is the output of π β β± on the
input π· β β³. The function π can quite naturally give the program size for each π β β±. If we
redefine the domain of π to be β³ Γ β±, we can let π(π·, π) be for example the running time of
the program π on the input π·, or the length of the computation (or derivation) table.
Given a logic, we define the equivalence relation β‘ β β± Γ β± such that (π, π β² ) β β‘ if and
only if π£(π, π) = π£(π β² , π) for all π β β±. We shall now define four formal problems relating
to explainability. The problems do work especially well for finite π, but this is not required
as long as the elements of π are representable in the sense that they can be used as inputs to
computational problems.
Definition 4. Let πΏ = (β³, β± , π£, π) be a logic. We define the following four problems for πΏ.
General explanation problem:
Input: π β β±, Output: π β β±
Description: Find π β β± with π β‘ π and minimal π(π ).
Special explanation problem
Input: (π, π, π) where π β β³, π β β± and π β π, Output: π β β± or e r r o r
Description: If π£(π, π) β π, output e r r o r . Else find π β β± with minimal π(π ) such that the
following two conditions hold:
(1) π£(π, π ) = π and
(2) For all πβ² β β³, π£(πβ² , π ) = π β π£(πβ² , π) = π.
General explainability problem
Input: (π, π), where π β β± and π β β, Output: Yes or no
Description: If there is π β β± with π β‘ π and π(π ) β€ π, output yes. Otherwise output no.
Special explainability problem
Input: (π, π, π, π) where π β β³, π β β±, π β π and π β β, Output: Yes or no
Description: Output βyesβ if and only if there exists some π β β± with π(π) β€ π such that the
conditions (1) and (2) of the special explanation problem hold.
In the full version, we shall generalize these definitions, but the current ones suffice here.
However, already in the current framework, the notions are quite flexible. Notice, for example,
that while the set β³ may typically be considered a set of models, or pieces of data, there are
many further natural possibilities. For instance, β³ can be a set of formulas. This nicely covers,
e.g., model-free settings based on proof systems.
3.1. Special explainability for PL
Let (π, π , π) be an input to the special explanation problem of propositional logic, where π
is a maximal conjunction w.r.t. some (any) finite Ξ¦ (thus encoding a Ξ¦-assignment) and π a
Ξ¦-formula. The special explanation problem can be reformulated equivalently in the following
way. (1) Suppose π = β€. If π β§ π, find a minimal interpolant between π and π. Else output e r r o r .
(2) Suppose π = β₯. If π β§ Β¬π, find a minimal interpolant between π and Β¬π. Else output e r r o r .
Let π β PL(Ξ¦) be a conjunction of literals. Let π(π) and π (π) be the sets of positive and
negative literals in π, respectively. We denote the De Morgan transformations of π and Β¬π by
DM(π) βΆ= β π β§ Β¬( β π) and DM(Β¬π) βΆ= Β¬( β π) β¨ β π.
πβπ(π) Β¬πβπ (π) πβπ(π) Β¬πβπ (π)
Lemma 5. Let Ξ¦ be a finite set of proposition symbols, let π be a maximal conjunction w.r.t. Ξ¦
and let π β PL(Ξ¦). (1) If π β§ π, then there is a subconjunction π of π such that DM(π ) is a minimal
interpolant between π and π. (2) If π β§ Β¬π, then there is a subconjunction π of π such that DM(Β¬π )
is a minimal interpolant between π and Β¬π.
Proof. Assume that π β§ π. Clearly at least one minimal interpolant exists, as for example π itself
is an interpolant. Let π be a minimal interpolant. Let Ξ¦(π) be the set of proposition symbols
occurring in π. We transform π into an equivalent formula π β² in Ξ¦(π)-full disjunctive normal
form where each disjunct is a maximal conjunction w.r.t. Ξ¦(π). To see that such a form always
exists, first consider the DNF of π and then, for each disjunct, fill in all possible values of any
missing propositions (thus possibly increasing the number of disjuncts).
Now, as π is a maximal conjunction w.r.t. Ξ¦, exactly one disjunct of π β² is a subconjunction of
π. Let π denote this disjunct. As π β§ π, the formula π is clearly an interpolant between π and π.
Now, each proposition in Ξ¦(π) occurs in π and thus also in DM(π ) exactly once, so DM(π )
has at most the same number of occurrences of proposition symbols and binary connectives as
π. Furthermore, DM(π ) has at most one negation. If π has no negations, then we claim DM(π )
also has none. To see this, note that π is a disjunct of π β² and π β² is equivalent to π, so π β§ π. As
π is negation-free, we have π β² β§ π where π β² is obtained from π by removing all the negative
literals. Hence, by the minimality of π, we have π β² = π. Thus π and DM(π ) are negation-free.
We have shown that size(DM(π )) β€ size(π), so DM(π ) is a minimal interpolant.
Suppose then that π β¨ Β¬π. Let π be a minimal interpolant between π and Β¬π. In a dual fashion
compared to the positive case above, we transform π into an equivalent formula π β² in Ξ¦(π)-full
conjunctive normal form. Additionally let π β² be the negation normal form of Β¬π. Now π β² is a
disjunction of literals and exactly one conjunct of π β² is a subdisjunction of π β² . Let π β² denote
this conjunct and let π denote the negation normal form of Β¬π β² . Now π is a subconjunction of π
and Β¬π is an interpolant between π and Β¬π.
As in the positive case, DM(Β¬π ) has at most the same number of proposition symbols and
binary connectives as the minimal interpolant π. The formula DM(Β¬π ) again has at most one
negation so we only check the case where π has no negations. Recall that Β¬π is equivalent
to π β² , which in turn is a conjunct of π β² . Thus π β¨ π β² . As π has no negations and π β² is a
disjunction of literals, we have π β¨ π β³ , where π β³ is obtained from π β² by removing all the
negative literals. By the minimality of π we obtain π β³ = π β² so π β² has no negations. Thus also
DM(Β¬π ) is negation-free and is a minimal interpolant.
The above lemma implies that for propositional logic, it suffices to consider subconjunctions
of the input in the special explanation and explainability problems. This will be very useful
both in the below theoretical considerations and in implementations.
π
We next prove Ξ£2 -completeness of the special explainability problem via a reduction from
π
Ξ£2 ππ΄π, which is well-known to be Ξ£2 -complete. The input of the problem is a quantified Boolean
formula π of the form βπ1 β¦ βππ βπ1 β¦ βππ π(π1 , β¦ , ππ , π1 , β¦ , ππ ). The output is yes iff π is true.
π
Theorem 6. The special explainability problem for PL is Ξ£2 -complete.
Proof. The upper bound is clear. For the lower bound, we will give a polynomial time (Karp-)
reduction from Ξ£2 ππ΄π. Consider an instance βπ1 β¦ βππ βπ1 β¦ βππ π(π1 , β¦ , ππ , π1 , β¦ , ππ ) of Ξ£2 ππ΄π.
We start by introducing, for every existentially quantified Boolean variable ππ , a new proposition
symbol ππ . Denoting π(π1 , β¦ , ππ , π1 , β¦ , ππ ) simply by π, we define
π π
π βΆ= β(ππ β¨ ππ ) β§ (π β¨ β(ππ β§ ππ )).
π=1 π=1
We let π be the valuation mapping all proposition symbols to 1, i.e., the assignment corresponding
π π
to the maximal conjunction ππ βΆ= βπ=1 (ππ β§ ππ ) β§ βπ=1 ππ w.r.t. the set of proposition symbols in
π. Clearly ππ β§ π. We now claim that there exists an interpolant of size at most 2π β 1 between
ππ and π iff the original instance of Ξ£2 ππ΄π is true.
Suppose first that the original instance of Ξ£2 ππ΄π is true. Thus there exists a tuple (π1 , β¦ , ππ ) β
{0, 1}π such that βπ1 β¦ ππ π(π1 , β¦ , ππ , π1 , β¦ , ππ ) is true. Consider now the subconjunction π βΆ=
βπ (ππ )=1 ππ β§ βπ (ππ )=0 ππ of ππ . Clearly π is of size 2π β 1. It is easy to see that π is also an
interpolant between ππ and π.
Suppose then that π is an interpolant of size at most 2π β 1 between ππ and π. Using Lemma
5, we can assume that π is a subconjunction of ππ . Since π has size at most 2π β 1, it can contain
at most π proposition symbols. Furthermore, π must contain, for every π β {1, β¦ , π}, either ππ or
π
ππ , since otherwise π would not entail βπ=1 (ππ β¨ ππ ). Thus π contains precisely π proposition
symbols. More specifically, π contains, for every π β {1, β¦ , π}, either ππ or ππ . Now, we define a
tuple (π’1 , β¦ , π’π ) β {0, 1}π by setting π’π = 1 if π contains ππ and π’π = 0 if π contains ππ . It is easy
to see that βπ1 β¦ ππ π(π’1 , β¦ , π’π , π1 , β¦ , ππ ) is true.
The above theorem immediately implies a wide range of corollaries. Recall that S5 is the sys-
tem of modal logic where the accessibility relations are equivalences. The special explainability
problem for S5 has as input a pointed S5-model (π, π€), an S5-formula π, π β {β€, β₯} and π β β.
π
Corollary 7. The special explainability problem for S5 is Ξ£2 -complete.
Proof. The lower bound follows immediately from Theorem 6, while the upper bound follows
from the well-known fact that the validity problem for S5 is coNP-complete [6].
π
Note indeed that the Ξ£2 lower bound for propositional logic is a rather useful result, implying
π
Ξ£2 -completeness of special explainability for various logics with an NP-complete satisfiability.
We next show that if the formula π in the special explainability problem is restricted to
CNF -formulas and we consider only the case π = β€, then the problem is NP-complete. The
following example demonstrates that it is necessary to restrict to the case π = β€.
Example 8. Let π β PL(Ξ¦) be an arbitrary CNF -formula and let π be a proposition symbol such
that π β Ξ¦. Suppose that π β π, where π (π) = 1 for every π β Ξ¦. Consider now the formula
ππ βΆ= π β¨ βπβΞ¦ Β¬π. Note that Β¬ππ is equivalent to a maximal conjunction w.r.t. Ξ¦ βͺ {π}. Clearly
π β§ Β¬π β§ ππ , since π entails that βπβΞ¦ Β¬π. We now claim that there exists an interpolant π of
size one between π β§ Β¬π and ππ iff π is unsatisfiable. First, we note that the only proposition
from Ξ¦ βͺ {π} which entails ππ is π. But the only way π can be an interpolant between π β§ Β¬π
and ππ is that π is unsatisfiable. Conversely, if π is unsatisfiable, then π is clearly an interpolant
between π β§ Β¬π and ππ . Since the unsatisfiability problem of CNF -formulas is coNP-hard, the
special explainability problem for CNF -formulas is also coNP-hard.
To prove NP-hardness, we will give a reduction from the dominating set problem. For a
graph πΊ = (π , πΈ), a dominating set π· β π is a set of vertices such that every vertex not in π·
is adjacent to a vertex in π·. The input of the dominating set problem is a graph and a natural
number π. The output is yes, if the graph has a dominating set of at most π vertices.
Theorem 9. For CNF -formulas, the special explainability problem with π = β€ is NP-complete.
The lower bound holds even if we restrict our attention to formulas without negations.
Proof. For the upper bound, let π β PL(Ξ¦) be a CNF -formula and let π be a maximal conjunction
w.r.t. Ξ¦. We want to determine whether there is an interpolant of size at most π. Using Lemma
5, it suffices to determine whether there is a subconjunction π of π such that size(DM(π )) β€ π.
Our nondeterministic procedure will start by guessing a subconjunction π of π. If
size(DM(π )) > π, then it rejects. Otherwise we replace the formula π with the formula π β²
which is obtained from π by replacing each proposition symbol π that occurs in π with either β€
or β₯, depending on whether π occurs positively or negatively in π. Now, if π β² is valid, then our
procedure accepts, and if it is not, then it rejects. Since the validity of CNF -formulas can be
decided in polynomial time, our procedure runs in polynomial time as well.
For the lower bound we will give a reduction from the dominating set problem. Consider a
graph πΊ = (π , πΈ) and a parameter π. Let
π βΆ= β (ππ£ β¨ β ππ’ ) (1)
π£βπ (π£,π’)βπΈ
and π βΆ= βπ£βπ ππ£ . Now π β§ π and π is a CNF -formula. It is easy to verify that there exists an
interpolant π of size at most 2π β 1 if and only if πΊ has a dominating set of size at most π.
By simply negating formulas, we obtain that the special explainability problem with π = β₯ is
NP-complete for DNF -formulas (and in general coNP-hard, see Example 8).
Corollary 10. For DNF -formulas, the special explainability problem with π = β₯ is NP-complete.
3.2. On general explainability
The general explainability problem for propositional logic has been discussed in the literature
under motivations unrelated to explainability. The minimum equivalent expression prob-
lem MEE asks, given a formula π and an integer π, if there exists a formula equivalent to π
π
and of size at most π. This problem has been shown in [7] to be Ξ£2 -complete under Turing
reductions, with formula size defined as the number of occurrences of proposition symbols and
with formulas in negation normal form. The case of standard reductions is open.
For logics beyond PL, the literature on the complexity of formula minimization is surprisingly
scarce. The study of formula size in first-order and modal logics has mainly focused on particular
properties that either can be expressed very succinctly or via a very large formulas. This leads to
relative succinctness results between logics. For lack of space, we shall not discuss the general
explainability problem further in the current article, but instead leave the topic for the future.
4. Implementation
In this section, we devise a proof-of-concept implementation of explainability problems defined
above. The implementation exploits the ASP fragment of the Clingo system1 combining the
Gringo grounder with the Clasp solver. However, we adopt the modular approach of [8] for
the representation of oracles, thus hiding disjunctive rules and their saturation from encodings.
Since CNF -formulas are dominant in the context of SAT checking, we devise our first imple-
mentation under an assumption that input formulas take this form. Thus, in spirit of Lemma 5,
π is essentially a set πΏ of literals and π is a set π of clauses, i.e., disjunctions of literals. To enable
meta-level encodings in ASP, a CNF -formula in DIMACS format can be reified into a set of
first-order (ground) facts using the lpreify tool2 (option flag - d ). Using additional rules, we
define domain predicates c l a u s e / 1 , p c o n d / 2 , and n c o n d / 2 for identifying clauses, their positive
conditions, and negative conditions respectively. The literals in the set πΏ are expressed by using
domain predicates p l i t / 1 and n l i t / 1 for positive and negative literals, respectively.
1
https://potassco.org/clingo/
2
https://github.com/asptools/software
Listing 1: Checking Positive Precondition (Lemma 5)
1 :- clause(C), nlit(P): pcond(C,P); plit(N): ncond(C,N).
2 simp(C) :- plit(P), pcond(C,P). simp(C) :- nlit(N), ncond(C,N).
3 simp(C) :- pcond(C,A), ncond(C,A).
4 :- clause(C), not simp(C), pcond(C,P), not plit(P), not nlit(P).
5 :- clause(C), not simp(C), ncond(C,N), not plit(N), not nlit(N).
Listing 2: Checking Negative Precondition (Lemma 5)
1 t(A) :- plit(A), atom(A).
2 { t(A) } :- atom(A), not plit(A), not nlit(A).
3 :- clause(C), not t(P): pcond(C,P); t(N): ncond(C,N).
We relax the requirement that the set of literals πΏ is maximal, so that any three-valued
interpretation can be represented. However, the precondition for the positive (resp. negative)
explanation is essentially the same: the result π β£πΏ of partially evaluating π with respect to πΏ must
remain valid (resp. unsatisfiable) in accordance to Lemma 5. The positive check is formalized in
Listing 1. The constraint in Line 1 excludes the possibility that πΏ falsifies π directly. Lines 2β3
detect which clauses of π are immediately true given πΏ and removed from π β£πΏ altogether. Rules
in Lines 4 and 5 deny any clause containing yet open literals that could be used to falsify the
clause in question. The net effect is that the encoding extended by facts describing πΏ and π has
an answer set iff π β£πΏ is valid. Since the scope of negation is restricted to domain predicates only,
the check is effectively polytime. The negative case can be handled by a single ASP program
evaluating a coNP query, see Listing 2. The rule in Line 1 infers any positive literal in πΏ to be
true while the negative ones in πΏ remain false by default. In Line 2, the truth values of atoms
undefined in πΏ are freely chosen. The constraint in Line 3 ensures that each clause in the input
π must be satisfied. Thus π β£πΏ is unsatisfiable iff the encoding extended by facts describing πΏ and
π has no answer set. In general, this check is deemed worst-case exponential, but for maximal
πΏ, the task reduces to simple polytime propagation as no choices are active in Line 2.
Our more general goal is to find minimum-size explanations πΏβ² β πΏ possessing the identical
property as required from πΏ, i.e., π β£πΏβ² is either valid or unsatisfiable. As regards the size of
πΏβ² , we leave the mapping back to a minimum-size formula as a post-processing step. In the
negative case (the second item of Lemma 5), the idea is formalized by Listing 3. While the (fixed)
set πΏ is specified as before using predicates p l i t / 1 and n l i t / 1 , the subset πΏβ² is determined by
choosing πΏ-compatible truth values for atoms in Line 1. The resulting size of πΏβ² is put subject
to minimization in Line 3 if k = 0 , as set by default in Line 2. Positive values k > 0 set by the user
activate the special explainability mode: the size of πΏβ² is at most k by the cardinality constraint
in Line 4. Besides this objective, we check that πΏβ² βͺ π is unsatisfiable by using an oracle encoded
in Listing 4. The input atoms (cf. [8]) are declared in Line 1. The predicate e t / 1 captures a
two-valued truth assignment compatible with πΏβ² as enforced by Lines 2 and 3. Moreover, the
clauses of π are satisfied by constraints introduced in Line 4. Thus, the oracle has an answer set
Listing 3: Finding Minimum-Size or Bounded-Size Explanations
1 { t(A) } :- atom(A), plit(A). { f(A) } :- atom(A), nlit(A).
2 #const k=0.
3 #minimize { 1,A: t(A), k=0; 1,A: f(A), k=0}.
4 :- #count { A: t(A); A: f(A)} > k, k>0.
Listing 4: Oracle for the Negative Case
1 { t(A) } :- plit(A). { f(A) } :- nlit(A).
2 et(A) :- t(A).
3 { et(A) }:- not t(A), not f(A), atom(A).
4 :- clause(C), not et(P): pcond(C,P); et(N): ncond(C,N).
Listing 5: Extension for the Positive Case
1 simp(C) :- t(P), pcond(C,P). simp(C) :- f(N), ncond(C,N).
2 simp(C) :- pcond(C,A), ncond(C,A).
3 :- clause(C), not simp(C), pcond(C,P), not t(P), not f(P).
4 :- clause(C), not simp(C), ncond(C,N), not t(N), not f(N).
iff πΏβ² βͺ π is satisfiable. However, stable-unstable semantics [9] and the translation unsat2lp from
[8] yield the complementary effect, amounting to the unsatisfiability of π β£πΏβ² .
On the other hand, the positive case (the first item of Lemma 5), can be covered by extending
the program of Listing 3 by further rules in Listing 5. The rules are analogous to those in
Listing 1, but formulated in terms of predicates t / 1 and f / 1 rather than p l i t / 1 and n l i t / 1 . Thus
πΏβ² inherits the properties of πΏ, i.e., the encoding based on Listings 3 and 5 extended by facts
describing πΏ and π has an answer set iff π β£πΏβ² is valid for a minimum-size πΏβ² β πΏ.
5. Experiments
In what follows, we evaluate the computational performance of the Clingo system by using
the encodings from Section 4 and two benchmark problems,3 viz. the famous π-queens (π-
Qs) problem and the dominating set (DS) problem of undirected graphsβrecall the proof of
Theorem 9 in this respect. Besides understanding the scalability of Clingo in reasoning tasks
corresponding to explanation problems defined in this work, we get also some indications what
kinds of explanations are obtained in practice. We study explainability in the context of these
benchmark problems to be first encoded as SAT problems in CNF using the declarative approach
from [10]: clauses involved in problem specifications are stated with rules in ASP style, but
interpreted in CNF by using an adapter called Satgrnd. Thus, the Gringo grounder of Clingo
3
https://github.com/asptools/benchmarks
Listing 6: Propositional Specification for the π-Queens Problem
1 #const n=8.
2 pair(X1,X2) :- X1=1..n, X2=X1+1..n.
3 triple(X1,X2,Y1) :- pair(X1,X2), Y1=1..n-(X2-X1).
4 queen(X,Y): Y=1..n :- X=1..n.
5 -queen(X,Y1) | -queen(X,Y2) :- X=1..n, pair(Y1,Y2).
6 -queen(X1,Y) | -queen(X2,Y) :- pair(X1,X2), Y=1..n.
7 -queen(X1,Y1) | -queen(X2,Y1+X2-X1) :- triple(X1,X2,Y1). % X1+Y2 = X2+Y1
8 -queen(X1,Y1+X2-X1) | -queen(X2,Y1) :- triple(X1,X2,Y1). % By symmetry
Listing 7: Propositional Specification for the Dominating Set Problem
1 vertex(X) :- edge(X,Y). vertex(Y) :- edge(X,Y).
2 in(X) | in(Y): edge(X,Y) | in(Z): edge(Z,X) :- vertex(X).
can be readily used for the instantiation of the respective propositional schemata, as given in
Listings 6 and 7, for subsequent SAT solving.
Our π-Qs encoding in Listing 6 introduces a default value for the number of queens n in
Line 1 and, based on n , the pairs and triples of numbers relevant for the construction of clauses
are formed in Lines 2 and 3. Then, for the queen in a column X , the length n clause in Line 4
chooses a row Y made unique for X by the clauses introduced in Line 5. Similarly, columns
become unique by the clauses in Line 6. Finally, queens on the same diagonal are denied by
clauses resulting from Lines 7 and 8. Turning our attention to the DS problem in Listing 7,
vertices are extracted from edges in Line 1. The clauses generated in Line 2 essentially capture
the disjunctions collected as parts of π in (1): our encoding assumes that the edges of the graph
are provided as ordered pairs for the sake of space efficiency. Intuitively, given any vertex X in
the graph, either it is in the (dominating) set or any of its neighboring vertices is.
In the experiments, we evaluate the performance of the Clasp solver (v. 3.3.5) when used to
solve various explainability problems. All test runs are executed on a cluster of Linux machines
with Intel Xeon 2.40 GHz CPUs, and a memory limit of 16 GB. We report only the running times
of the solver, since the implementations of grounding and translation steps are suboptimal due
to our meta-level approach and such computations could also be performed off-line in general,
and it is worth emphasizing that our current method has been designed to work for any CNF
and set of literals given as input. For π-Qs, we generate (i) positive instances by searching for
random solutions to the problem with different values of π and (ii) negative instances by moving,
in each solution found, one randomly selected queen to a wrong row. The respective truth
assignments are converted into sets of literals πΏ ready for explaining. For DS, we first generate
random planar graphs of varying sizes and search for minimum-size dominating sets for them.
Then, negative instances are obtained by moving one random vertex outside each optimal set
and by describing the outcomes as sets of literals πΏ. For positive instances, we include the
positive literal i n ( X ) in πΏ for all vertices X , in analogy to the reduction deployed in Theorem 9.
10 4 10 3
10 2
10 2
10 2 10 1
Time (s)
Time (s)
Time (s)
10 0
10 0
10 0 10 -1
10 -2
10 -2
10 -2 10 -3
100 200 300 400 500 10 15 20 25 30 35 40 45 50 8 10 12 14 16 18 20 22 24
Number of Nodes Number of Nodes Number of Queens
(a) (b) (c)
Figure 1: Experimental Results on Explaining DS Positively (a), Negatively (b), and π-Qs Negatively (c).
The results of our experiments are collected in Figure 1. Since initial screening suggests that
explanation under exact size bounds is computationally more difficult, we present only results
obtained by minimizing the size of πΏ using the Clasp solver in its unsatisfiable core (USC) mode.
Figure 1a shows the performance of Clasp when searching for positive explanations for DS based
on planar graphs from 100 up to 550 vertices. Explanations are minimum-size dominating sets.
The performance obtained for the respective negative explanations is presented in Figure 1b.
In spite of somewhat similar scaling, far smaller planar graphs with the number of vertices in
the range 10 β¦ 50 can be covered. In this case, explanations consist of sets of vertices based on
some vertex and its neighbors. The final plot in Figure 1c concerns π-Qs when π = 8 β¦ 24 and
negative explanations are sought. Explanations obtained from the runs correspond to either (i)
single (misplaced) queens or (ii) pairs of (threatening) queens. The respective positive instances
simply reproduce solutions and are computationally easy. Therefore, they are uninteresting.
Some observations are in order. The instances obtained by increasing their size, i.e., either
the number of vertices or queens, give rise to higher running times almost systematically. For
each size, the time is computed as an average for running 10 instances of equal size. Due to
logarithmic scale, running times tend to scale exponentially. Moreover, positive explanations
appear to be easier to find than negative ones in compliance with complexity results.
6. Conclusion
We have provided general, logic-based definitions of explainability and studied the particular
case of propositional logic in detail. The related Ξ£π2 -completeness result gives a useful, robust
lower bound for a wide range of more expressive logics and future work. We have also shown
NP-completeness of the explainability problems with formulas in CNF and DNF when the input
truth value is restricted. Moreover, we have presented a proof-of-concept implementation for
the explanation of CNF -formulas (without truth value restrictions). Our experimental results
confirm the expected worst-case exponential runtime behavior of Clasp. Negative explanations
have higher computational cost than positive explanations. The optimization variants of
explanation problems seem interesting, because the USC strategy seems very effective and the
users need not provide fixed bounds for queries in advance.
References
[1] G. Brewka, T. Eiter, M. Truszczynski, Answer set programming at a glance, Commun.
ACM 54 (2011) 92β103. doi:1 0 . 1 1 4 5 / 2 0 4 3 1 7 4 . 2 0 4 3 1 9 5 .
[2] P. Simons, I. NiemelΓ€, T. Soininen, Extending and implementing the stable model semantics,
Artif. Intell. 138 (2002) 181β234. doi:1 0 . 1 0 1 6 / S 0 0 0 4 - 3 7 0 2 ( 0 2 ) 0 0 1 8 7 - X .
[3] T. Eiter, G. Gottlob, On the computational cost of disjunctive logic programming: Proposi-
tional case, Ann. Math. Artif. Intell. 15 (1995) 289β323. doi:1 0 . 1 0 0 7 / B F 0 1 5 3 6 3 9 9 .
[4] A. Shih, A. Choi, A. Darwiche, A symbolic approach to explaining Bayesian network
classifiers, in: J. Lang (Ed.), IJCAI, 2018, pp. 5103β5111. doi:1 0 . 2 4 9 6 3 / i j c a i . 2 0 1 8 / 7 0 8 .
[5] C. Umans, The minimum equivalent DNF problem and shortest implicants, J. Comput.
Syst. Sci. 63 (2001) 597β611. doi:1 0 . 1 0 0 6 / j c s s . 2 0 0 1 . 1 7 7 5 .
[6] P. Blackburn, M. de Rijke, Y. Venema, Modal Logic, volume 53 of Cambridge Tracts in Theo-
retical Computer Science, Cambridge University Press, 2001. doi:1 0 . 1 0 1 7 / C B O 9 7 8 1 1 0 7 0 5 0 8 8 4 .
[7] D. Buchfuhrer, C. Umans, The complexity of Boolean formula minimization, J. Comput.
Syst. Sci. 77 (2011) 142β153. doi:1 0 . 1 0 1 6 / j . j c s s . 2 0 1 0 . 0 6 . 0 1 1 .
[8] T. Janhunen, Implementing stable-unstable semantics with ASPTOOLS and clingo, in:
J. Cheney, S. Perri (Eds.), PADL, 2022, pp. 135β153. doi:1 0 . 1 0 0 7 / 9 7 8 - 3 - 0 3 0 - 9 4 4 7 9 - 7 \ _ 9 .
[9] B. Bogaerts, T. Janhunen, S. Tasharrofi, Stable-unstable semantics: Beyond NP with
normal logic programs, Theory Pract. Log. Program. 16 (2016) 570β586. doi:1 0 . 1 0 1 7 /
S1471068416000387.
[10] M. Gebser, T. Janhunen, R. Kaminski, T. Schaub, S. Tasharrofi, Writing declarative
specifications for clauses, in: L. Michael, A. C. Kakas (Eds.), JELIA, 2016, pp. 256β271.
doi:1 0 . 1 0 0 7 / 9 7 8 - 3 - 3 1 9 - 4 8 7 5 8 - 8 \ _ 1 7 .
Acknowledgments
Tomi Janhunen, Antti Kuusisto, Masood Feyzbakhsh Rankooh and Miikka Vilander were sup-
ported by the Academy of Finland consortium project Explaining AI via Logic (XAILOG), grant
numbers 345633 (Janhunen) and 345612 (Kuusisto). Antti Kuusisto was also supported by the
Academy of Finland project Theory of computational logics, grant numbers 324435, 328987 (to
December 2021) and 352419, 352420 (from January 2022). The author names of this article have
been ordered on the basis of alphabetic order.