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.
This paper investigates explainability in a general setting. The key in our approach is to relate explainability to formula size. We diferentiate 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 https://reijojaakkola.github.io/ (R. Jaakkola); https://tuni.fi/en/tomi-janhunen (T. Janhunen); 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) [
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 efective, 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 [
In [
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 .
In this section we introduce four natural problems concerning the general and special perspectives 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.
be a logic. We define the following four problems for .
Definition 4. Let = (ℳ, ℱ , , ) 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 ( ) 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 () ≤ conditions (1) and (2) of the special explanation problem hold.
In the full version, we shall generalize these definitions, but the current ones sufice 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.
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 sufices 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. Σ2
We next prove Σ2 -completeness of the special explainability problem via a reduction from , 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 if 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 interpolant between and .
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 if 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 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 ∶= ⋀( ∨ ) ∧( ∨ ⋁( ∧ )).
=1 =1 to see that ∀ 1 … ( 1, … , , 1, … , ) is true. 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
The above theorem immediately implies a wide range of corollaries. Recall that S5 is the system 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 [
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 if 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 sufices 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.
The general explainability problem for propositional logic has been discussed in the literature
under motivations unrelated to explainability. The minimum equivalent expression
problem 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 [
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.
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 [
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).
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 efect is that the encoding extended by facts describing and has an answer set if ∣ is valid. Since the scope of negation is restricted to domain predicates only, the check is efectively 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 if 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. [
Listing 3: Finding Minimum-Size or Bounded-Size Explanations
{ f(A) } :- atom(A), nlit(A).
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). 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).
simp(C) :- f(N), ncond(C,N).
if ′ ∪ is satisfiable. However, stable-unstable semantics [
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 if ∣ ′ is valid for a minimum-size ′ ⊆ .
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 [
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 eficiency. 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 of-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 diferent 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. 102 () s e m iT100 103 102 )101 s (e100 m i T 10-1 10-2 100 200 Number of Nodes 300 400 (a) 500
The results of our experiments are collected in Figure 1. Since initial screening suggests that explanation under exact size bounds is computationally more dificult, 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.
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 efective and the users need not provide fixed bounds for queries in advance.