Gilles Audemard
email: audemard@cril.fr

Frédéric Koriche
email: koriche@cril.fr

Pierre Marquis
email: marquis@cril.fr

On Tractable XAI Queries based on Compiled Representations

One of the key purposes of eXplainable AI (XAI) is to develop techniques for understanding predictions made by Machine Learning (ML) models and for assessing how much reliable they are. Several encoding schemas have recently been pointed out, showing how ML classifiers of various types can be mapped to Boolean circuits exhibiting the same inputoutput behaviours. Thanks to such mappings, XAI queries about classifiers can be delegated to the corresponding circuits. In this paper, we present some explanation queries and verification queries about classifiers. We show how they can be addressed by combining queries and transformations about the associated Boolean circuits. Taking advantage of previous results from the knowledge compilation map, this allows us to identify a number of cases for which XAI queries are tractable provided that the circuit has been first turned into a compiled representation.

Introduction

In the past decade, ML techniques have revolutionized vision, speech, language understanding, and many other fields. However, the most powerful ML models (e.g., deep neural nets) in term of quality of predictions are poorly explainable. For such black boxes, it is humanly impossible to understand the sequence of operations which are performed for predicting the label of an input instance. Thus, explaining the predictions made by such ML models (i.e., why a given instance is classified as such?) is not feasible in general. Assessing the robustness of the predictions (i.e., would a small change in the input instance question the predicted label?) is also out of reach. In essence, the impossibility to explain predictions and to determine the extent to which they are reliable forms a major obstacle in a number of applications for which safety is of paramount importance (like autonomous cars or medical diagnosis).

This calls for explanation technologies, enabling for reasoning about the decisions made by the classifier, measuring how robust they are, testing whether the classifier is biased and how much it complies with some prior knowledge about classes, etc. Accordingly, there has been a growing body of work on explainable and robust AI (XAI) for the past couple of years [START_REF] Katz | The marabou framework for verification and analysis of deep neural networks[END_REF][START_REF] Ignatiev | Abduction-based explanations for machine learning models[END_REF][START_REF] Bunel | A unified view of piecewise linear neural network verification[END_REF][START_REF] Leofante | Automated verification of neural networks: Advances, challenges and perspectives[END_REF][START_REF] Molnar | iml: An R package for interpretable machine learning[END_REF]Shih, Darwiche, and Choi 2019;[START_REF] Guidotti | A survey of methods for explaining black box models[END_REF][START_REF] Miller | Explanation in artificial intelligence: Insights from the social sciences[END_REF][START_REF] Molnar | Interpretable Machine Learning -A Guide for Making Black Box Models Explainable[END_REF]. In this research topic, recent works have shown how ML classifiers C of various types (including black boxes) can be associated with Boolean circuits Σ (alias transparent or "white" boxes), exhibiting the same input-output behaviours [START_REF] Narodytska | Verifying properties of binarized deep neural networks[END_REF]Shih, Choi, and Darwiche 2018a;Shih, Choi, and Darwiche 2019). Thanks to such mappings, XAI queries about classifiers can be delegated to the corresponding circuits (Darwiche and Hirth 2020). The rationale for this approach is twofold: on the one hand, Σ as an abstraction of C is typically far less complex than C; on the other hand, the Boolean nature of Σ makes it amenable to various reasoning tasks required for generating explanations and addressing reliability issues.

The present study is relevant to this research trend within XAI. Our objective is to state in a formal way a number of XAI queries about C and for each of them, to identify some sufficient conditions on the language L used to represent Σ that render the query tractable. For the sake of generality, we do not make any strong assumption on the nature of the classifier: C can be a feedforward neural network, a Bayesian network classifier, a random forest, etc. We just assume that C is a discrete multi-label classifier from which a Boolean circuit Σ having the same input-output behaviour can been generated. More precisely, each input instance is a vector x of n values assigned to Boolean features from a set X = {x 1 , • • • , x n } and each corresponding output is a vector y ∈ Y of m values taken from a set Y = {y 1 , • • • , y m } of Boolean labels. 1 Given the prediction y = C(x), the instance x ∈ X is classified by C as an element of the jth class if and only if y j = 1.

The variables of Σ are split into three categories: (1) Input variables used to describe the input features of C.

Each input variable is a Boolean variable from X;

(2) Output variables used to describe classes or labels. Each output variable is a Boolean variable from Y ;

1 When an input feature xi is not Boolean, but takes values into a finite domain {v1, • • • , vp}, one can represent it using p Boolean features x 1 i , • • • , x p i so that x j i is true if and only if xi takes value vj. The direct -or sparse -encoding [START_REF] De Kleer | A comparison of ATMS and CSP techniques[END_REF][START_REF] Walsh | SAT v CSP[END_REF] of xi is given by the constraints p-1 j=1 p k=j+1 (¬x j i ∨ ¬x k i ) and p j=1 x j i ensuring that xi takes exactly one value in its domain.

(3) Intermediate variables used to capture all other features of the classifier C, and corresponding to the wires of Σ that are not output ones. Each intermediate variable is also assumed to take a Boolean value, and we use Z to denote the set of those variables.

As Σ and C are supposed to have the same input-output behaviour, for any pair (x, y) for which y = C(x), we have y j = 1 precisely when the output variable y j of the circuit Σ on the input x is set to 1. Importantly, we make no assumption about the number of predicted labels: for an input x, several coordinates -resp. no coordinate -of the associated output y can be set to 1, which means that C (and hence Σ) recognizes x as a member of several (resp. no) class(es).

In practice, C is often associated with additional information about y, taking the form of weights representing confidences or probabilities about predicted labels. Such weights are usually exploited by the encoding scheme for generating Σ from C, but they are not encoded into Σ. Thus, Σ is viewed as a compact representation of the classes Y , as they are recognized by C.

In the following, we present a number of XAI queries of practical interest for explaining classifications achieved by C, or for assessing the robustness of C. These queries are addressed by considering the circuit Σ associated with C, instead of C itself. For the sake of clarity, we split XAI queries into explanation queries and verification queries. Explanation queries are concerned by the local interpretability issue, i.e., they are about a given input x, while verification queries are concerned by the global interpretability issue, i.e., they are independent of any input. Some of the XAI queries considered in the following are brand new, others have been introduced in the recent past. In both cases, we show how these explanation and verification queries can be modeled using basic operations over Boolean circuits. Taking advantage of previous results from the knowledge compilation map for propositional languages L [START_REF] Darwiche | A knowledge compilation map[END_REF], this allows us to identify a number of XAI queries which are tractable, provided that the circuit Σ has been first turned into a compiled representation from L.

The rest of the paper is organized as follows. After some formal preliminaries about propositional logic and the knowledge compilation map, we present a simple encoding schema that can be used to associate a Boolean circuit Σ with a given random forest C over Boolean features. A toy example is provided, that will serve as a running example for illustrating the XAI queries presented afterwards. Then, we successively present some explanation queries and some verification queries, and for each of them, we identify some sufficient conditions on the propositional language used to represent Σ which ensure that the query is tractable (i.e., it can be answered using a polynomial-time algorithm). Finally, we discuss the results and conclude the paper.

Formal Preliminaries

Propositional Languages. The languages considered in this paper are defined over a finite set PS of propositional variables and a finite set of connectives. The elements of a propositional language L are called representations, and for any such representation Σ, we denote by Var (Σ) the subset of variables of PS occurring in Σ. As usual, atomic representations include propositional variables in PS , and Boolean constants in { , ⊥}. A literal is a propositional variable, possibly negated, or a Boolean constant. Any propositional variable x is called a positive literal, and the negation of x, denoted ¬x or x, is called a negative literal. A term is a conjunction of literals, and a clause is a disjunction of literals.

Given a set of variables X ⊆PS , an interpretation over X is a mapping ω from X to B = {0, 1}. Propositional representations are interpreted in a classical way. For a representation Σ and an interpretation over X = Var (Σ), we use ω |= Σ to denote the fact that ω if a model of Σ according to the semantics of propositional logic. That is, assigning the variables of Σ to truth values as specified by ω makes Σ true. By [Σ] we denote the set of models of Σ over Var (Σ), and by Σ we denote the number of models of Σ over Var (Σ). In particular, Σ is inconsistent if Σ = 0,

and consistent otherwise. A representation Σ 2 is a logical consequence of a representation Σ 1 (denoted Σ 1 |= Σ 2 ) if Σ 1 ∧¬Σ 2 is inconsistent. Σ 1 and Σ 2 are logically equivalent (denoted Σ 1 ≡ Σ 2 ) if they are logical consequences of each other.
Given a representation Σ and a consistent term γ, the conditioning of Σ by γ is the representation obtained by replacing in Σ every occurrence of a variable x ∈ Var (γ) by if x is a positive literal of γ and by ⊥ if ¬x is a negative literal of γ. Finally, when X is a subset of propositional variables from PS , Σ is said to be independent of X if there is a representation Φ logically equivalent to Σ such that Var (Φ) ∩ X = ∅. The forgetting of X in Σ, denoted ∃X.Σ, is the most general consequence of Σ that is independent of X (see e.g., [START_REF] Lang | Propositional independence: Formula-variable independence and forgetting[END_REF]). The projection of Σ onto X is the forgetting of X in Σ, where X denotes the set PS \X. We mention in passing that ∃X.Σ can be computed as a propositional representation, thanks to the following inductive characterization:

• ∃∅.Σ ≡ Σ, • ∃{x}.Σ ≡ (Σ | ¬x) ∨ (Σ | x), • ∃(X ∪ {x}).Σ ≡ ∃X .(∃{x}.Σ).
Knowledge Compilation Map. Introduced by [START_REF] Darwiche | A knowledge compilation map[END_REF], and extended in a number of papers (e.g., [START_REF] Darwiche | Compiling propositional weighted bases[END_REF][START_REF] Niveau | Knowledge compilation using interval automata and applications to planning[END_REF][START_REF] Darwiche | SDD: A new canonical representation of propositional knowledge bases[END_REF][START_REF] Fargier | Towards a knowledge compilation map for heterogeneous representation languages[END_REF][START_REF] Fargier | Disjunctive closures for knowledge compilation[END_REF][START_REF] Koriche | Fixed-parameter tractable optimization under DNNF constraints[END_REF])), the knowledge compilation (KC) map is a multicriteria evaluation of propositional languages. Various languages have been considered as target languages for knowledge compilation. They include, among others, DNF (disjunctions of terms), DNNF (decomposable normal form circuits) [START_REF] Darwiche | Decomposable negation normal form[END_REF], FBDD (free binary decision diagrams) [START_REF] Gergov | Efficient analysis and manipulation of OBDDs can be extended to FBDDs[END_REF], and OBDD (ordered binary decision diagrams) [START_REF] Bryant | Graph-based algorithms for Boolean function manipulation[END_REF]). In the KC map, a propositional language L is evaluated according to properties it offers, or not, depending on the existence of a polynomial-time algorithm for achieving some treatment of interest. These properties are usually decomposed into queries and transformations. In this paper, we focus on the following queries and transformations: ) into a representation from L for which the models are those of Σ minimizing the value of f . We also add to the list of properties the following trans-2 Actually, this requirement is stronger than the one considered in [START_REF] Darwiche | A knowledge compilation map[END_REF] which only required that the set of models can be enumerated in time polynomial in the size of Σ plus the size of the corresponding set of models. Note that we have that L satisfies ME (in the strong sense) whenever it satisfies CD and CO (see [START_REF] Fargier | Disjunctive closures for knowledge compilation[END_REF] for details). formation that will be useful in the rest of the paper: -decomposable conjunction: L satisfies ∧DC if and only if there is a polynomial-time algorithm that maps

k rep- resentations Σ 1 , • • • , Σ k from L such that Var (Σ i ) ∩ Var (Σ j ) = ∅ (for i, j ∈ {1, • • • , k}, i = j) to a repre- sentation from L that is logically equivalent to k i=1 Σ i .
In the KC map, the space efficiency or succinctness of propositional languages is also assessed. Informally, the succinctness captures the relative ability of propositional languages to encode pieces of information using little space. For example, it is known that DNNF is strictly more succinct than OBDD and DNF. A language suited for a given application is then viewed as one of the most succinct languages offering the queries and transformations required by the application [START_REF] Darwiche | A knowledge compilation map[END_REF].

Encoding Random Forests

In order to illustrate the approach into which our work takes place and the forthcoming XAI queries, let us first explain how to associate a Boolean circuit Σ with a given random forest C over Boolean features (the proposed encoding is quite easy).

A decision tree (here, a classification tree) [START_REF] Breiman | Classification and Regression Trees[END_REF][START_REF] Quinlan | Induction of decision trees[END_REF]) is a finite tree T where each internal node is a decision node labelled by a feature x from X and having as many children as the cardinality of the domain of x, and each leaf node is labelled by a non-empty subset of Y . The arcs from a decision node to its children are labelled by pairs noted x = v where v is an element of the domain of the feature x labelling the node (one value v per arc). A path of T is a (finite) sequence of labels x = v of the arcs encountered from the root of T to one of its leaves. A decision tree classifies an input x as an element of class y j ∈ Y if the unique path of T that is compatible with x (i.e., that contains a pair x = v only if x takes the value v in x) leads to a leaf node whose label contains y j .

A random forest R [START_REF] Ho | The random subspace method for constructing decision forests[END_REF][START_REF] Breiman | Bagging predictors[END_REF][START_REF] Breiman | Random forests[END_REF]) is a finite set of p decision trees over the set X of features. Given a threshold τ ∈ {1, . . . , p}, a random forest R = {T 1 , . . . , T p } classifies an input x as y j ∈ Y if at least τ decision trees of R classifies x as y j .

Example 1. As a matter of example, consider a fruit classification task and the random forest R given by the trees T 1 , T 2 and T 3 , illustrated in Figure 1. Each decision tree is defined over the set of input features X = {SW(eet taste), GR(een), RO(und shape)}, and the set of output labels Y = {GRA(pe fruit), BAN(ana), APP(le)}. An instance x is classified as a label y ∈ Y if and only if it is classified as such by a strict majority of decision trees in R (i.e., at least τ = 2 decision trees of R classify x as y).

In Figure 1, the labels x = v of the arcs are not explicitly represented. A dashed line from a decision node labelled by x corresponds to the label x = 0, while a plain line corresponds to the label x = 1.

Based on this example, the input instance x 1 given by (SW = 0, GR = 0, RO = 0) is classified by T 1 (resp. T 2 , T 3 ) as an element of GRA (resp. GRA or BAN, BAN). The instance x 2 defined by

(SW = 1, GR = 1, RO = 0) is classi- fied by T 1 (resp. T 2 , T 3
) as an element of GRA (resp. BAN, BAN). Thus, R classifies x 1 as an element of GRA or BAN, and R classifies x 2 as an element of BAN.

Note that R may remain mute about a given instance, meaning that there is no evidence enough to classify it as any element of Y . For instance, R does not predict anything about the input instance (SW = 1, GR = 1, RO = 1), since this input is classified by T 1 (resp. T 2 , T 3 ) as an element of GRA (resp. BAN, APP). Thus, the strict majority threshold of 2 is not met for this instance.

Based on these considerations, let us present an encoding schema which maps any random forest R, defined on the input variables X and the output variables Y , to a representation Σ over the set of propositional variables PS = X ∪ Y ∪ Z, where Z captures the intermediate variables.

Σ is the conjunction of two kinds of constraints:

• for every j ∈ {1, . . . , m}, Σ includes the constraint

y j ⇔ p k=1 z k j ≥ τ
where variable z k j is true if and only if the input instance x is classified as an element of class y j by T k . Accordingly, the input is classified as y j by R if and only if the number of decision trees of R classifying x as an element of y j is at least equal to the threshold τ ;

• for every j ∈ {1, . . . , m} and every k ∈ {1, . . . , p}, Σ

SW GR RO GRA BAN APP 0 0 0 1 1 0 0 0 1 1 0 0 0 1 0 0 1 0 0 1 1 0 0 1 1 0 0 0 1 0 1 0 1 0 0 1 1 1 0 0 1 0 1 1 1 0 0 0 Table 1: The projection of Σ over X ∪ Y .
includes a constraint

z k j ⇔   γ∈Γ(T k ,yj ) γ  
indicating that z k j is set to true (i.e., x is classified as an element of y j by T k ) if and only if x is compatible with a path of T k leading to a leaf node labelled by y j . Here, Γ(T k , y j ) denotes the set of all terms γ encoding the paths of T k which lead to leaf nodes labelled by y j . For our running example, R is associated with the representation Σ, which is given by the conjunction of the following constraints:

GRA ⇔ (GRA 1 + GRA 2 + GRA 3 ≥ 2) BAN ⇔ (BAN 1 + BAN 2 + BAN 3 ≥ 2) APP ⇔ (APP 1 + APP 2 + APP 3 ≥ 2) GRA 1 ⇔ ((SW ∧ GR) ∨ (SW ∧ GR)) BAN 1 ⇔ ((SW ∧ GR ∧ RO) ∨ (SW ∧ GR ∧ RO)) APP 1 ⇔ ((SW ∧ GR ∧ RO) ∨ (SW ∧ GR ∧ RO)) GRA 2 ⇔ ((SW ∧ GR ∧ RO) ∨ (SW ∧ GR ∧ RO)) BAN 2 ⇔ ((SW ∧ GR ∧ RO) ∨ (SW ∧ GR ∧ RO) ∨(SW ∧ GR)) APP 2 ⇔ ((SW ∧ GR ∧ RO) ∨ (SW ∧ GR ∧ RO)) GRA 3 ⇔ (SW ∧ GR ∧ RO) BAN 3 ⇔ RO APP 3 ⇔ ((SW ∧ GR ∧ RO) ∨ (SW ∧ RO))
From Σ, the following constraints expressing how each class is inferred from the input features can be derived as logical consequences:

GRA ⇔ (SW ∧ GR) BAN ⇔ RO APP ⇔ ((SW ∧ GR) ∨ (SW ∧ GR)) ∧ RO
Equivalently, the projection of Σ onto X ∪ Y is given by the truth assignments in Table 1.

XAI Queries

After illustrating how multi-labels classifiers can be encoded into propositional representations, we are now in position to examine XAI queries. We first present a couple of results, showing how the notion of membership of an instance x to a class of Y as predicted by C can be translated in logical terms when Σ (represented using a propositional language L) is considered instead of C.

To this point, observe that any input instance x of the form (x 1 = v 1 , . . . , x n = v n ) can be encoded as a term over the literals on X, also denoted x to avoid heavy notations. Specifically, x is given by n j=1 j where j = x j if v j = 1 and j = x j otherwise. Now, since Σ has the same input-output behaviour as C, we know that every variable from Y ∪ Z is defined in Σ in terms of X. In other words, for any input x, we have C(x) = (y 1 = c 1 , . . . , y m = c m ) if and only if the unique model of Σ over X ∪ Y ∪ Z which is compatible with x assigns to each output variable y j (j ∈ {1, . . . , m}) the truth value c j . Being "defined" means here that for any variable u ∈ Y ∪ Z there exists a formula ϕ u built upon variables of X, only, that is such that Σ |= u ⇔ ϕ u [START_REF] Beth | On Padoa's method in the theory of definition[END_REF][START_REF] Lang | On propositional definability[END_REF].

Based on these notions, the input instances x which are classified by C as elements of class y j in the sense that y j = 1 when C(x) = (y 1 = c 1 , . . . , y m = c m ) can be characterized in several ways using Σ:

• abductive characterization: x is an abductive explanation of y j with respect to Σ provided that the set of assumptions is the set of all literals over the variables from X. Indeed, if y j is true in C(x) then we have Σ ∧ x |= y j . Note here that Σ ∧ x is consistent for every input instance x over X, since Σ is a Boolean circuit with inputs in X.

• model-based characterization: x is a model over X of ∃X.(Σ ∧ y j )
, or equivalently a model over X of ∃X.(Σ | y j ). Thus, the projection of Σ | y j onto X can be viewed as a compact representation of all the input instances x viewed as elements of y j by C.

Verification Queries

As indicated above, the XAI queries under consideration in this study are separated into verification and explanation queries. We start with the verification queries.

Counting the inputs (CIN) / enumerating the inputs (EIN) associated with a given class. These queries are useful for a user in order to figure out the classes of Y as they are recognized by C (which may differ from what the user has in mind). For instance, in our running example, the user might be surprised by the fact that the instance given by SW ∧ GR ∧ RO is classified as an element of GRA, and hence, she would like to gather more information about instances labeled by this class. Proposition 1. Counting the inputs associated by C with a given class is in P when L satisfies CD and CT. Enumerating those inputs with polynomial delay is feasible when L satisfies CD and ME.

Proof. Counting the inputs x associated by C with a given output y j amounts to computing Σ | y j . Enumerating those inputs boils down to enumerating the models of ∃X.(Σ | y j ) with polynomial delay, which is feasible as soon as L satisfies CD, FO, and ME. Since every variable of Var (Σ) not belonging to X is defined from X in Σ, we can just enumerate the models of Σ | y j , filtering out from each of them all the literals over the intermediate variables from Z. Thus, the enumeration query is tractable as soon as L satisfies CD and ME.

Counting the inputs (CAM) / enumerating the inputs (EAM) for which the classifier provides ambiguous outputs / remains mute. The CAM query is important for estimating how resolute the classifier C is. Indeed, as much C provides ambiguous outputs or remains mute for input instances, as much it will be hard to take advantage of it for making decisions. The EAM query is also useful, as it points out instances for which ambiguities or omissions arise. In our running example, only one instance, given by the term SW ∧ GR ∧ RO, is ambiguously classified by C. Similarly, only one instance, given by SW ∧ GR ∧ RO, is not recognized by C as a member of any class from Y .

Proposition 2. Counting the inputs for which C provides ambiguous outputs / remains mute is in P when L satisfies CD and CT. Enumerating with polynomial delay the inputs that are ambiguously recognized by C as elements of the intersection of a given set of classes / the inputs for which C remains mute, is feasible when L satisfies CD and ME.

Proof. Counting the inputs for which C remains mute amounts to computing A = Σ | m j=1 y j . Furthermore, the number of inputs mapped by C into a single class y j is given by B j = Σ | (y j ∧ k∈{1,...,m}|k =j y k ) . Therefore, counting the number of inputs for which C provides ambiguous outputs amounts to evaluating |X| -Am j=1 B j . The instances classified as elements of the intersection of a given set S ⊆ Y of classes are given by the models over X of Σ | γ S , where γ S = yj ∈S y j , and those for which C remains mute correspond to the models over X of Σ | m j=1 y j . Thus, they can be enumerated with polynomial delay from Σ when L satisfies CD and ME.

Measuring the frequency of some feature in a given class (MFR) / identifying mandatory or forbidden features (IMA). MFR aims to evaluate how significant is the presence of each feature x k in each class of interest y j . More generally, one can consider a combination of features (each of them being either present or absent) instead of a single feature being present. We can also consider a combination of classes (again, each of them being either met or not). When the frequency is equal to 1, x k is mandatory for being recognized as an element of y j , while when it is equal to 0, it is forbidden for being recognized as an element of y j . In our running example, the frequency of SW (resp. GR, RO) in class APP is 1 2 (resp. 1 2 , 1). Thus, none of the three features is forbidden for the class of apples, but having a round shape (RO) is mandatory.

Proposition 3.

• Computing the frequency of a feature (or a combination of features) in a given class (or combination of classes) is in P when L satisfies CD and CT. • Deciding whether a feature (or a combination of features) is mandatory or forbidden in a given class (or combination of classes) is in P when L satisfies CD and CO.

Proof.

• The frequency of x k in y j is given by

Σ|(yj ∧x k ) Σ|yj
. When a more complex combination of features / classes is considered, it is sufficient to replace the terms y j ∧ x k (resp. y j ) in this equation by the terms denoting the combination of features and classes (resp. classes) to get the right value. This value can be computed in polynomial time when L satisfies CD and CT.

• Determining whether x k is mandatory (resp. forbidden) for y j amounts to deciding whether or not Σ | (y j ∧ x k ) is inconsistent (resp. Σ | (y j ∧ x k ) is inconsistent), which can be achieved in polynomial time when L satisfies CD and CO. When a more complex combination of features / classes is considered, one consistency test per feature must be done, replacing y j by the combination of classes under consideration. Since the combination of features is part of the input, the problem can still be solved in polynomial time when L satisfies CD and CO.

Identifying irrelevant features for a given class (IIR). In many scenarios, the user has some beliefs about the features that must be relevant (or not), for some classes. For instance, she might expect that the shape of a fruit is relevant for determining whether it is a banana -this is indeed the case in our running example. Dually, the user could believe that a given class should not depend on some features, which otherwise would reveal a bias in the classifier. For instance, she might expect that the class of bananas should not depend on GR -again, this is the case in our running example.

Recall that an input feature x i is irrelevant for a class y j if the value of x i can be switched without changing the fact that the instance is predicted by the classifier as an element of y j . Stated otherwise, the membership in y j of any instance x does not depend on the value of its feature x i . Proposition 4. Determining the features that are considered as useless by C for a given class is in P whenever L satisfies CD, FO, and EQ.

Proof. x i is irrelevant for y j if and only if ∃X.(Σ | y j ) is independent from x i [START_REF] Lang | Propositional independence: Formula-variable independence and forgetting[END_REF]. This amounts to testing whether (∃X.(Σ | y j )) | x i and (∃X.(Σ | y j )) | ¬x i are equivalent, or not. This can be done in polynomial time when L satisfies CD, FO, and EQ. When considering Boolean features, this proposition coheres with a result reported in (Shih, Choi, and Darwiche 2018a), showing that identifying irrelevant features is tractable when an OBDD representation of ∃X.(Σ | y j ) is provided.

Identifying monotone/anti-monotone features (IMO).

In many applications, it is believed that increasing the value of some feature does not change the membership to some class. Dually, one might also expect that decreasing the value of another feature does not change the membership to that class. For example, if a given fruit with a non-green color is recognized as an apple, then switching its color to green should not change the fact that it is still an apple. By contrast, if a fruit with sweet taste is recognized as a grape, then it is reasonable to expect that it would remain a grape fruit if its taste was sour (i.e., not sweet).

In more formal terms, a classifier C is monotone (resp. anti-monotone) for a given class y j , with respect an input feature x i , if for any input instance x such that C(x) = y with y j = 1 implies that C(x[x i ← 1]) = y (resp. C(x[x i ← 0]) = y ) with y j = 1.3 Proposition 5. Checking whether the classifier is monotone (or anti-monotone) for a class y j with respect to an input feature x i is in P whenever L satisfies CD, FO, and SE.

Proof. At the semantics level, conditioning a propositional representation ϕ by a literal (resp. ¬ ) consists first in selecting the models ω of ϕ over Var (ϕ) where is assigned to 1 (resp. 0), then in forgetting in the result (which leads to add to this set of models every interpretation that coincides with one of the ω but is such that is assigned to 0 (resp. 1) in it). Using symbols, ϕ | x ≡ ∃{x}.(ϕ ∧ x) and ϕ | x ≡ ∃{x}.(ϕ ∧ x). Accordingly, if C is not monotonic (resp. anti-monotonic) for y j with respect to x i , then there is a model of ∃X.(Σ | y j ) which is not a model of ∃X.(Σ | y j ) conditioned by x i (resp. x i ). Thus, checking whether C is monotonic (resp. anti-monotonic) for y j w.r.t. x i amounts to testing whether ∃X.

(Σ | y j ) |= (∃X.(Σ | y j )) | x i (resp. ∃X.(Σ | y j ) |= (∃X.(Σ | y j )) | x i ).
This can be done in polynomial time when L satisfies CD, FO, and SE.

In our running example, one can check that the random forest R is monotonic for the class GRA with respect to the feature SW. We mention in passing that the notion of monotonicity has already been considered in (Shih, Choi, and Darwiche 2018a) for binary classifiers (i.e., when m = 1).

Determining how much classes are close to each other (MCJ, MCH). In multi-label classification, the user may have some beliefs about the extent to which the classes of Y are close to each other. For example, it can be expected that the class of apples is at least as close to the class of grape fruits as to the class of bananas. Thus, it is interesting to determine whether or not the closeness of classes (as they are identified by the predictor) is compatible with those beliefs. Such a consideration requires a formal characterization of the notion of "similarity".

A simple, yet poorly informative notion of similarity is ordinal and takes the form of a set of pre-orders ≤ yj over Y , one for each class j ∈ {1, • • • , m}. By writing y k ≤ yj y l , we mean that y k is at least as close to y j as to y l . Thus, the user may believe that APP ≤ GRA BAN. Of course, it is expected that y j ≤ yj y l whatever y l ∈ Y . Clearly enough, every cardinal similarity σ between classes of Y (i.e., a symmetric mapping associating a non-negative number with a couple of classes), induces an ordinal similarity given by y k ≤ yj y l if and only if σ(y k , y j ) ≥ σ(y l , y j ).

Several cardinal similarities can be defined and evaluated from Σ. A first one is given by the Jaccard index J(y k , y l ): it is the number of elements belonging to both classes, divided by the number of elements belonging to at least one of them (i.e., the cardinality of the intersection of the two classes divided by the cardinality of their union). J(y k , y l ) indicates the proportion of inputs that are (possibly wrongly) recognized as both y k and y l among those which are recognized as belonging to at least one of the two classes. J(y k , y l ) varies between 0 and 1, the higher the more similar y k and y l . When classes are not given explicitly as the sets of their elements but represented implicitly using a circuit Σ as done in our setting, we get:

J(y k , y l ) = Σ ∧ (y k ∧ y l ) Σ ∧ (y k ∨ y l )
Clearly, when the classes y k and y l are pairwise disjoint (as it should be for apples and bananas, ideally) one must have J(y k , y l ) = 0. In the running example, we can check from Table 1 that J(BAN, GRA) = 1 5 while J(APP, GRA) = 0. Thus, from the point of view of Jaccard index, bananas are viewed as closer to grape fruits than apples, which can be considered as counter-intuitive by the user and reflect a problem in the predictor.

Sometimes, it makes sense to evaluate the distance between two classes y k and y l as an aggregation of a more elementary distance between the elements of the two classes. For example, we can take the Hamming distance between an element of y k and an element of y l . 4 In doing so, let d H (x, x ) denote the number of bits that differ between the inputs x and x from X. This distance can be easily lifted to propositional representations Σ 1 and Σ 2 over X encoding sets of such inputs:

5 d H (Σ 1 , Σ 2 ) = min ω1∈[Σ1] min ω2∈[Σ2] d H (ω 1 , ω 2 )
and then the cardinal similarity H between classes can be defined as follows:

H(y k , y l ) = n -d H (∃X.(Σ | y k ), ∃X.(Σ | y l ))
n Thus, H(y k , y l ) gives the proportion of (Boolean) features that do not need to be switched to go from an element of y k to an element of y l . In the running example, we can check from Table 1 that H(BAN, GRA) = 1 (since both classes share an element) while H(APP, GRA) = 2 3 . From the point of view of H similarity, bananas are also viewed as closer to grape fruits than apples. Proposition 6.

• MCJ: computing J(y k , y l ) is in P when L satisfies CD and CT. • MCH: computing H(y k , y l ) is in P when L satisfies CD, ∧BC, ∧DC, OPT, and ME.

Proof.

• As to J(y k , y l ), it is enough to observe that J(y k , y l ) is also equal to

Σ | (y k ∧ y l ) Σ | (y k ∧ y l ) + Σ | (y k ∧ y l ) + Σ | (y k ∧ y l )
.

• The computation of H(y k , y l ) is a bit more subtle. Consider a representation Σ in L and a "clone" Σ of it obtained by renaming (in a uniform way) every variable v occurring in Σ into v . Then condition Σ by y k and Σ by y l , and compute a representation α in L of the conjunction of the resulting representations. This can be done in time polynomial in the size of Σ when L satisfies CD and ∧BC. The next step consists in computing a representation in L of each formula z i ⊕ (x i ⇔ x i ) where i ∈ {1, • • • , n} and z i is a fresh variable of PS . This can be done in constant time since every such formula has a fixed size and involves only 3 variables. Then since L satisfies ∧DC, a representation β in L of n i=1 (z i ⊕ (x i ⇔ x i )) can be computed in polynomial time. Finally, a representation γ in L of α ∧ β can be computed in polynomial time when L satisfies ∧BC. Consider now a linear function f over Var (α ∧ β) associating with every variable in it the weight 0, except the variables z 1 , • • • , z n that have weight 1. Since L satisfies OPT, a representation δ in L having for models those of γ minimizing the value of f can be computed in polynomial time from γ and f . By construction, every such model contains a minimum number of variables z i set to 1, and this number is equal to d H (∃X.(Σ | y k ), ∃X.(Σ | y l )) (note the the projection onto the variables of X is done implicitly by the optimization transformation when the variables out of X are given a null weight in the linear function). Because L satisfies ME, a model ω of δ can be generated in polynomial time. Once computed, it is enough to count the number of variables z i set to 1 in it to get d H (∃X.(Σ | y k ), ∃X.(Σ | y l )), from which H(y k , y l ) can be easily derived.

Computing how far a class is from a given prototype (MCP). In many cases, the user has in mind a prototypical element of the class. For instance, she may believe that an apple has a round shape, is not green, and has a sweet taste, which yields to the prototype SW ∧ GR ∧ RO. Based on this background information, it is interesting to determine how much each class (as it is recognized by C) complies with this prototype, which can be evaluated by computing the Hamming distance between every element of the class and the prototype, and considering the maximal distance. In our running example, the instance SW ∧ GR ∧ RO classified as an apple by R coincides with the prototype, while the other instance SW ∧ GR ∧ RO classified as an apple by R is at a distance of 2 from the prototype SW ∧ GR ∧ RO. Thus the distance of the class of apples (as they are recognized by R) to the corresponding prototype is 2. A large value of this distance can be considered as unacceptable, as it may reflect a bias in the data used to train C. Proposition 7. Computing how far a given class y j is from a given prototype x is in P when L satisfies CD, OPT, and ME.

Proof. The approach for computing this value is as follows. One first generates a representation α in L of Σ | y j , which is feasible in polynomial time when L satisfies CD. Assuming that

x = (x 1 = v 1 , • • • , x n = v n ),
one then considers a linear function f x that associates a null weight with every variable from Y ∪ Z, and with every x i (i ∈ {1, • • • , n}), a weight equal to -1 if v i = 1 and a weight equal to 1 when v i = 0. Accordingly, for every truth assignment ω over X ∪ Y ∪ Z, we have that f x (ω) + Σ n i=1 v i is equal to the Hamming distance between the projection of ω onto X and x. Since Σ n i=1 v i does not depend on ω, the projections onto X of the interpretations ω maximizing the value of f x are those maximizing the Hamming distance to x. Obviously enough, they are also (precisely) the projections onto X of the interpretations ω minimizing the value of -f x , which is a linear function as well. When L satisfies OPT, a representation β from L of the models of α minimizing the value of -f x can be computed in polynomial time. Finally, when L satisfies ME, a model ω of β can be generated in polynomial time; the Hamming distance between the projection of ω onto X and x is the maximal distance between an element of the class y j and x, i.e., the value we look for.

Explanation Queries

We now turn to explanation queries, which are related to a specific input x and the way it has been classified by C. Often, the reason why x has been classified as an element of a class y j does not depend on all features over X but only on some of them. This leads to the two following notions of minimum-cardinality explanations and of prime implicant explanations introduced in (Shih, Choi, and Darwiche 2018b). When the prediction achieved by C is somewhat unexpected, the user may also ask for counterfactual explanations. Whatever the type of explanation that is looked for (minimum-cardinality, prime implicant, counterfactual), an input instance can have exponentially many explanations.

Enumerating

minimum-cardinality explanations (EMC). Given an input x such that C(x) = y with y j = 1, a minimum-cardinality explanation of x classified as an y j is an input instance x such that C(x ) = y with y j = 1 (i.e., x is classified as an y j as well), x coheres with x on the ones in the sense that for any k ∈ {1, . . . , n}, if x k = 1 then x k = 1, and x has a minimal number of coordinates set to 1. Roughly speaking, the features that are set to 1 in x are enough to explain why x has been classified by C as an element of y j . In our running example, a minimum-cardinality explanation of input SW ∧ GR ∧ RO (classified as an element of BAN by R) is RO. Proposition 8. The minimum-cardinality explanations of x can be enumerated with polynomial delay from Σ given y j as soon as L satisfies CD, OPT, and ME.

Proof. First, one computes in polynomial time a representation α in L of Σ | y j . Then one considers the linear function f associating with every variable in Y ∪ Z the weight 0, except the variables of X that have weight 1. Since L satisfies OPT, a representation β in L having for models those of α minimizing the value of f can be computed in polynomial time from β and f . By construction, the projection of every such model onto X is a minimum-cardinality explanation of x. Furthermore, since every variable from Y ∪ Z is defined from X in Σ, two distinct models of β over Var (β) necessarily have two distinct projections onto X. Thus, enumerating the models of β and projecting each of them onto X as soon as it is generated leads to enumerating the minimumcardinality explanations of x. The fact that L satisfies ME is therefore enough to conclude the proof.

The above proposition extends a result from (Shih, Choi, and Darwiche 2018b), where it was shown that the enumeration of minimum-cardinality explanations is feasible with a polynomial delay when L = OBDD. Indeed, OBDD satisfies CD, OPT, and ME, but many other languages in the DNNF family (including DNNF itself) are strictly more succinct than OBDD and also satisfy those properties.

Note that mandatory features are relevant to minimumcardinality explanations in the sense that every minimumcardinality explanation of x necessarily contains every feature that is mandatory for being recognized as an element of y j by C. Similarly, no irrelevant feature for y j participates in any minimum-cardinality explanation.

Deriving a prime implicant explanation (DPI). Given an input x such that C(x) = y with y j = 1, a prime implicant explanation is a subset-minimal partial assignment x which is coherent with x (i.e., x and x give the same values to the variables that are assigned in x ) and which satisfies the property that for every extension x of x over X, we have C(x ) = y with y j = 1. The features assigned in x (and the way they are assigned) can be viewed as explaining why x has been classified as an element of y j . Thus, in the running example, a prime implicant explanation of input SW ∧ GR ∧ RO (classified as an element of GRA by R) is SW ∧ GR. The fact that RO holds or not does not matter.

Proposition 9. Deriving a prime implicant explanation of x from Σ given y j is in P when L satisfies CD, FO, and IM.

Proof. The computation of a prime implicant explanation of x is a follows. First, compute a representation α in L of ∃X.(Σ | y j ). This is feasible in polynomial time since L is supposed to satisfy CD and FO. Then, the problem amounts to computing a prime implicant of α. This can be done in polynomial time using a greedy algorithm when L satisfies IM: start with x, which is a model (hence an implicant) of α, and for every literal of x, test in polynomial time whether x deprived from this literal is still an implicant of the formula (this is feasible in polynomial time when L satisfies IM); if the resulting term still is an implicant of α, then remove the literal, otherwise keep it and resume.

Prime implicant explanations are also referred to as sufficient reasons for a decision in [START_REF] Darwiche | On the reasons behind decisions[END_REF]. Interestingly, the explanations of classifications as produced by Anchor [START_REF] Ribeiro | Anchors: High-precision model-agnostic explanations[END_REF] can be viewed as approximations of prime implicant explanations [START_REF] Narodytska | Assessing heuristic machine learning explanations with model counting[END_REF]. Note that every prime implicant explanation of x contains every feature that is mandatory for being recognized as an element of y j by C. Furthermore, no prime implicant explanation of x contains a feature that is forbidden or irrelevant for being recognized as an element of y j by C (if ∃X.(Σ | y j ) is independent from x k , x k does not occur in any prime implicant of ∃X.(Σ | y j )). Finally, it can be noted that discrete, yet non-Boolean features raise some representation issues when dealing with prime implicant explanations (it turns out that the prime implicants over the Boolean features obtained using the direct encoding do not capture the intended explanations, see [START_REF] Choi | On symbolically encoding the behavior of random forests[END_REF]).

From a computational point of view, the enumeration of prime implicant explanations looks as a much more demanding issue than the enumeration of minimum-cardinality explanations. Though algorithms for computing the set of prime implicant explanations exist (see (Shih, Choi, and Darwiche 2018b;[START_REF] Darwiche | On the reasons behind decisions[END_REF]), the question of the existence of an algorithm with polynomial delay for enumerating the elements of this set from a representation Σ ∈ L is open for many L (e.g., L = OBDD) as far as we know. Especially, though the enumeration of the models of Σ with a polynomial delay is possible as soon as L satisfies CD and CO [START_REF] Darwiche | A knowledge compilation map[END_REF], those conditions on L do not appear as sufficient for ensuring the existence of an enumeration algorithm with polynomial delay for the prime implicants of Σ. Indeed, it is known that unless P = NP there is no input-output polynomial time algorithm for generating the prime implicants of a monotone formula [START_REF] Goldsmith | Complexity of DNF and isomorphism of monotone formulas[END_REF], and the language of monotone formulae satisfies CD and CO.

Enumerating counterfactual explanations (ECO). Occasionally, the user may be surprised by the way C has classified a given instance x 1 . She was expecting the input instance to be recognized as an apple (y k ), but it has been classified as a grape fruit (y j ). In such a case, the user is likely to ask for a counterfactual explanation: one is interested in identifying an instance x 2 which is classified as an apple (and not as a grape fruit), and is as close as possible to x 1 in terms of the number of common values of the features in the two inputs (alias the Hamming distance d H (x 1 , x 2 )). Indeed, the set of features that differ in x 1 and x 2 can be viewed as an explanation of why x 1 has not been classified as y k . In the running example, an input classified as an element of APP and that is as close as possible to

x 1 = SW ∧ GR ∧ RO w.r.t. d H is SW ∧ GR ∧ RO (it is at Ham- ming distance 2 of SW ∧ GR ∧ RO). Another counterfactual explanation for x 1 is SW ∧ GR ∧ RO.
Proposition 10. The counterfactual explanations of x can be enumerated with polynomial delay from Σ given y j and y k as soon as L satisfies CD, OPT, and ME.

Proof. One first generates a representation α in L of Σ | (y k ∧ y j ), which is feasible in polynomial time when L satisfies CD. Then one considers the same function f x as in the proof of Proposition 7. For every truth assignment ω over X ∪ Y ∪ Z, the value f x (ω) + Σ n i=1 v i is equal to the Hamming distance between the projection of ω onto X and x. Since Σ n i=1 v i does not depend on ω, the projections onto X of the interpretations ω minimizing the value of f x are those minimizing the Hamming distance to x. When L satisfies OPT, a representation β from L of the models of α minimizing the value of f x can be computed in polynomial time.

In addition, when L satisfies ME, starting from β, those models can be enumerated with a polynomial delay. Since every variable from Y ∪ Z is defined from X in Σ, two distinct models of β over Var (β) necessarily have two distinct projections onto X. Hence the counterfactual explanations of x can be enumerated with a polynomial delay.

As a direct consequence of Proposition 10, when L satisfies CD, OPT, and ME, one can easily compute the robustness (Shih, Choi, and Darwiche 2018a) of the classification of x as an y j defined as min k=1,...,m|k =j d H (x, Σ | (y k ∧ y j )), i.e., the Hamming distance between x and a closest instance that has been recognized by C as belonging to a class distinct from y j . In essence, this amounts to computing in sequence a counterfactual explanation of x for every y k distinct from y j , and for each of them to compute its Hamming distance to x while memorizing the minimum distance. The computation of this robustness can clearly be done in polynomial time, extending to the Boolean case a result from (Shih, Choi, and Darwiche 2018a) in which it is shown that this is indeed the case for L = OBDD (which satisfies CD, OPT, and ME).

Discussion

The XAI queries considered in the paper correspond to computation problems of various types: decision problems (IMA, IIR, IMO), counting problems (CIN, CAM), function problems (DPI, MFR, MCJ, MCH, MCP), enumeration problems (EMC, ECO, EIN, EA). Whatever its type, each of those queries is NP-hard in the broad sense [START_REF] Garey | Computers and intractability: a guide to the theory of NP-completeness[END_REF] when no restrictions are imposed on the circuit Σ (i.e., when one just assumes that Σ is a circuit with inputs in X, outputs in Y , and intermediate variables in Z). More precisely, we can prove that for any of the queries associated with decision, counting, or function problems, if a polynomial-time algorithm for solving the query existed, then we would have P = NP. In addition, we can also prove that for any of the queries associated with an enumeration problem, if an algorithm for enumerating solutions with polynomial delay existed, then we would have P = NP. Thus, making additional assumptions on Σ looks as mandatory to make tractable any of the 14 XAI queries listed in Table 2. This is the path followed in the paper. Indeed, the results reported in the previous propositions identify conditions under which the XAI queries are tractable, those conditions taking the form of queries and transformations offered by the language L used to represent Σ.

To make such results significant from the practical side, two conditions must be fulfilled. On the one hand, some encoding schemas associating a circuit with a given classifier must be available. This is already the case for several families of classifiers, including Bayes classifiers [START_REF] Chan | Reasoning about bayesian network classifiers[END_REF]Shih, Choi, and Darwiche 2019), binary neural networks [START_REF] Narodytska | Verifying properties of binarized deep neural networks[END_REF]Shih, Darwiche, and Choi 2019;[START_REF] Shi | On tractable representations of binary neural networks[END_REF], and random forests (as shown in the paper). On the other hand, languages L satisfying the queries and transformations supporting the XAI queries under consideration must exist and translators (alias compilers) for generating representations in L of Σ must be implemented. Hopefully, this is also the case.

In this respect, the family of DNNF languages [START_REF] Darwiche | Decomposable negation normal form[END_REF][START_REF] Huang | The language of search[END_REF][START_REF] Pipatsrisawat | New compilation languages based on structured decomposability[END_REF][START_REF] Oztok | On compiling CNF into Decision-DNNF[END_REF]) appears as particularly interesting. A DNNF representation Σ is a Boolean circuit with a single root, internal nodes labelled by connectives in {∧, ∨}, leaves labeled by literals over PS or Boolean constants, and satisfying the following decomposability condition: the DNNF representations rooted at any ∧-node in Σ do not share any variable. A d-DNNF representation is a DNNF representation Σ that satisfies the following determinism condition: the d-DNNF representations rooted at any ∨-node in Σ are pairwise inconsistent.

A Decision-DNNF representation Σ is a Boolean circuit with a single root, leaves are labeled by literals over PS or Boolean constants, and internal nodes are decomposable ∧nodes or decision nodes of the form ite(x, n 1 , n 2 ), where ite stands for "if ... then ... else ...". In a decision node ite(x, n 1 , n 2 ), x is any propositional variable of PS (the decision variable), and the Decision-DNNF representations Σ 1 and Σ 2 rooted (respectively) at n 1 and n 2 do not contain any occurrence of x. ite can be considered as a ternary connective so that every node of the form ite(x, n 1 , n 2 ) can be viewed as a short for (x ∧ Σ 1 ) ∨ (x ∧ Σ 2 ). Since in the latter statement, the ∧-nodes are decomposable nodes, and the ∨-node is a deterministic one, every Decision-DNNF circuit can be considered as a d-DNNF circuit. Formally, there exists a linear-time equivalence-preserving translation from Decision-DNNF to d-DNNF. Structural restrictions on DNNF circuits based on a concept of vtree can also be imposed, leading to languages of structured DNNF representations that offer additional queries and transformations.

Thanks to the decomposability/determinism/structure conditions, languages of the DNNF family offer many queries and transformations of interest. 6 Thus, DNNF satisfies CD, CO, FO, OPT, ∧DC, and d-DNNF offers all the queries and transformations listed in the paper, except SE, EQ, FO, ∧BC [START_REF] Darwiche | A knowledge compilation map[END_REF][START_REF] Darwiche | Compiling propositional weighted bases[END_REF]. Structured d-DNNF circuits (given a fixed vtree) offers in addition SE, EQ, and ∧BC. Accordingly, under the restriction when Σ is given as a DNNF circuit (resp. a d-DNNF circuit), the XAI queries EMC, ECO, EIN, IMA, and MCP (resp. CIN, MFR, and MCJ) are tractable. MCH is tractable when Σ is given as a structured d-DNNF circuit. Finally, though Decision-DNNF does not offer FO in the general case, wherever the forgetting transformation is used for solving the XAI queries considered above, it concerns variables that are defined from unforgotten ones (those of X). In such a case, applying the forgetting algorithm that consists in replacing every decision node labelled by a variable from X by a ∨-node (while keeping the same two children) turns the Decision-DNNF cir-6 In addition, DNNF languages are quite succinct -actually, more than other candidates like OBDD or FBDD [START_REF] Darwiche | A knowledge compilation map[END_REF][START_REF] Bova | Knowledge compilation meets communication complexity[END_REF]) -, and there exist compilers targeting those languages when Σ is given at start as a CNF formula [START_REF] Darwiche | Decomposable negation normal form[END_REF][START_REF] Darwiche | New advances in compiling CNF into decomposable negation normal form[END_REF][START_REF] Pipatsrisawat | Top-down algorithms for constructing structured DNNF: Theoretical and practical implications[END_REF][START_REF] Muise | Dsharp: Fast d-DNNF compilation with sharpSAT[END_REF][START_REF] Lagniez | An Improved Decision-DNNF Compiler[END_REF] cuit at hand into a d-DNNF circuit (see [START_REF] Lagniez | Definability for model counting[END_REF] for details). As a consequence, DPI is tractable when Σ is given as a Decision-DNNF circuit, and IIR and IMO are tractable when Σ is given as a structured Decision-DNNF circuit.

Conclusion

In this paper, we have presented a number of XAI queries, which are useful for explaining classifications achieved by a predictor C (the queries are EMC, DPI, ECO) or for assessing the robustness of C (the queries are CIN, EIN, CAM, EAM, MFR, IMA, IIR, IMO, MCJ, MCH, MCP). All those queries are delegated to a Boolean circuit Σ exhibiting the same input-output behaviour as C.

We have shown how these XAI queries can be addressed by combining operations on Boolean circuits. Especially, taking advantage of previous results reported in the knowledge compilation literature, we have identified some conditions on the language L used for representing Σ that prove enough for ensuring the tractability of the XAI queries. Table 2 summarizes the XAI queries considered in the paper and associates with each of them some conditions on L that are sufficient to make it tractable. Several subsets L of DNNF appear as valuable, ensuring that many XAI queries from the table are tractable whenever Σ is represented in L.

This work calls for many perspectives. Designing encoding schemas suited to other types of classifiers (e.g., other ensemble methods) is one of them. From the theory side, deriving bounds on the size of the compiled representations in various target languages of the corresponding encodings is an interesting issue we would like to address. From a more practical point of view, we plan to make experiments to determine the scalability of the compilation-based approach to XAI for several encoding schemas (associated with classifiers of various types) and for several target languages for knowledge compilation.

Figure 1 :

 1 Figure 1: A random forest with three decision trees T1, T2, T3.

Table 2 :

 2 .XAI query Conditions on L making the query tractable XAI queries and conditions on L that are sufficient to make them tractable.

	EMC	CD, OPT, ME
	DPI	CD, FO, IM
	ECO	CD, OPT, ME
	CIN	CD, CT
	EIN	CD, ME
	CAM	CD, CT
	EAM	CD, ME
	MFR	CD, CT
	IMA	CD, CO
	IIR	CD, FO, EQ
	IMO	CD, FO, SE
	MCJ	CD, CT
	MCH	CD, ∧BC, ∧DC, OPT, ME
	MCP	CD, OPT, ME

If x = (x1, • • • , xn), then x[x k ← v] is the same vector as x, except that the jth coordinate x k of x[x k ← v] has value v.

Note that the Hamming distance between two assignments of a feature xi over a finite, yet non-Boolean domain, can be computed as the weighted Hamming distance between the corresponding assignments of the Boolean variables x j i obtained using the direct encoding (just consider a weight of 1 2 for each x j i ).

 5 We define dH (Σ1, Σ2) = +∞ whenever Σ1 is inconsistent or Σ2 is inconsistent.

Acknowledgements

Many thanks to the anonymous reviewers for their comments and suggestions. This work has benefited from the support of the AI Chair EXPEKCTATION of the French National Research Agency (ANR).


Jean-Marie Lagniez
email: lagniez@cril.fr

Pierre Marquis Cril

A Recursive Algorithm for Projected Model Counting

We present a recursive algorithm for projected model counting, i.e., the problem consisting in determining the number of models ∃X.Σ of a propositional formula Σ after eliminating from it a given set X of variables. Based on a "standard" model counter, our algorithm projMC takes advantage of a disjunctive decomposition scheme of ∃X.Σ for computing ∃X.Σ . It also looks for disjoint components in its input for improving the computation. Our experiments show that in many cases projMC is significantly m ore e fficient th an the previous algorithms for projected model counting from the literature.

Introduction

In this paper, we are concerned with the projected model counting problem. Given a propositional formula Σ and a set X of propositional variables to be forgotten, one wants to compute the number of interpretations of the variables occurring in Σ but not in X, which coincide on X with a model of Σ. Stated otherwise, the objective is to count the number of models of the quantified Boolean formula ∃X.Σ over its variables (i.e., the variables occurring in Σ but not in X).

The projected model counting problem is a central issue to a number of AI problems (for instance, in planning, when the objective is to compute the robustness of a given plan given by the number of initial states from which the execution of the plan reaches a goal state [START_REF] Aziz | #∃SAT: Projected model counting[END_REF]), but also outside AI (especially it proves useful in some formal verification p roblems ( Klebanov, M anthey, a nd Muise 2013)).

Since it generalizes the standard model counting problem (recovered when X = ∅), the projected model counting problem is at least as hard as the latter (#P-hard). The presence of variables X to be forgotten nevertheless may render the problem easier in some cases (thus, when every variable of Σ belongs to X, the problem boils down to deciding the satisfiability of Σ). That mentioned, a naive approach which would consist first in forgetting the variables of X from Σ, then in counting the number of models of the resulting formula would be impractical in many cases, in particular when X is large. Indeed, forgetting the variables of X from Σ in a brute-force way often leads to a formula which is much larger than Σ (in the worst case, an exponential blow-up may occur).

Despite the importance of the problem, few algorithms for projected model counting have been pointed out so far. An FPT algorithm, where the parameter is the treewidth of the primal graph of the input instance, has been designed recently [START_REF] Fichte | Exploiting treewidth for projected model counting and its limits[END_REF], but this algorithm is practical only for instances having a very small treewidth. Three other algorithms for the projected model counting task have been presented in [START_REF] Aziz | #∃SAT: Projected model counting[END_REF], namely dSharp P , #clasp, and d2c. Those algorithms are quite dissimilar in essence:

• dSharp P is an adaptation of the model counter dSharp [START_REF] Muise | Dsharp: Fast d-DNNF compilation with sharpSAT[END_REF], which computes a Decision-DNNF representation of its input Σ to determine the number of models Σ . dSharp P considers as an additional input a set P of protected variables (i.e., those variables of Σ which should not be forgotten). The search achieved by dSharp is constrained so that the decision variables are taken in priority from P . Whenever there is no variable of P in the current formula (i.e., this formula contains only variables from X), a sat solver is used to determine whether it is consistent. If so, its number of models is 1, otherwise it is equal to 0. This technique has also been considered in [START_REF] Klebanov | SATbased analysis and quantification of information flow in programs[END_REF]. Note that the constraint imposed on the variable ordering limits the ability to find cutsets of small size, and this may have a strong (yet negative) impact on the quality of the conjunctive decompositions of Σ found by dSharp.

• #clasp is an extension of clasp, an algorithm for model enumeration on a projected set of variables [START_REF] Gebser | Solution enumeration for projected Boolean search problems[END_REF], which basically amounts to computing a deterministic DNF representation of ∃X.Σ.

Each time an implicant of ∃X.Σ is found, a blocking clause equivalent to the negation of this implicant is added to Σ. In #clasp, whenever an implicant of ∃X.Σ is found, a prime implicant is first extracted from it in a greedy fashion (this is reminiscent to the approach considered in [START_REF] Schrag | Compilation for critically constrained knowledge bases[END_REF][START_REF] Castell | Computation of prime implicates and prime implicants by a variant of the Davis and Putnam procedure[END_REF]). Compared to clasp, this further extraction step often leads to the adding of far less blocking clauses to Σ, so that #clasp performs usually better than clasp.

• d2c consists in computing first a Decision-DNNF representation of Σ, then forgetting in it all the variables of X (this can be achieved in linear time, but the resulting representation is not deterministic any longer in the general case). The next step consists in turning this resulting representation into a CNF one. This can be done in linear time via the introduction of new variables while preserving the number of models of the input [START_REF] Tseitin | On the complexity of derivation in propositional calculus[END_REF]). Finally, the number of models of the resulting CNF formula is evaluated using sharpSAT [START_REF] Thurley | sharpSAT -counting models with advanced component caching and implicit BCP[END_REF].

Unlike those algorithms, our algorithm for projected model counting, called projMC, is a recursive algorithm exploiting a disjunctive decomposition scheme of ∃X.Σ for computing ∃X.Σ . More precisely, ∃X.Σ is split into an equivalent (disjunctively interpreted) set of pairwise inconsistent formulae, so that ∃X.Σ can be computed by summing up the corresponding projected model counts. projMC also looks for disjoint components in its input for improving the computation.

To evaluate the performance of our approach, we measured the time required by projMC for achieving the projected model counting task on a number of benchmarks (uniform random 3-CNF formulae, random Boolean circuits, planning instances). Our experiments show that in many cases projMC challenges the previous algorithms for projected model counting from the literature. Indeed, for some benchmarks, when compared to dSharp P , #clasp, and d2c, the time savings achieved by projMC are of several orders of magnitude. In order to verify that the improvements obtained in practice with projMC are actually due to the underlying approach and not to the performance of the "standard" model counter used in it (which is D4 (Lagniez and Marquis 2017) in our implementation), we also developed D4 P , which is the same algorithm as dSharp P , but using D4 as a model counter instead of dSharp. While D4 P performs typically better than dSharp P (and #clasp and d2c), projMC appears as a better performer than D4 P for many instances.

The rest of the paper is organized as follows. In the next section, we give some formal preliminaries. Then we describe our new projected model counter. Afterwards we present the empirical protocol which has been considered in the experiments, as well as the corresponding experimental results. Finally, a last section concludes the paper and gives some perspectives for further research. The binary code of projMC, as well as the benchmarks used in our experiments and additional empirical results are available from www.cril.fr/KC/.

Formal Preliminaries

Let L P be a propositional language built up from a finite set of propositional variables P and the usual connectives. ⊥ (resp. ) is the Boolean constant always false (resp. true). An interpretation (or world) ω is a mapping from P to {0, 1}.The set of all interpretations is denoted W. An interpretation ω is a model of a formula ϕ ∈ L P if and only if it makes it true in the usual truth functional way. M od(ϕ) denotes the set of models of the formula ϕ, i.e., M od(ϕ) = {ω ∈ W | ω is a model of ϕ}. |= denotes log-ical entailment and ≡ logical equivalence, i.e., ϕ |= ψ iff M od(ϕ) ⊆ M od(ψ) and ϕ ≡ ψ iff M od(ϕ) = M od(ψ). When ϕ ∈ L P and X ⊆ P, ∃X.ϕ is a quantified Boolean formula denoting (up to logical equivalence) the most general consequence of ϕ which is independent from the variables of X (see e.g., [START_REF] Lang | Propositional independence: Formula-variable independence and forgetting[END_REF]). Var (ϕ) denotes the set of variables occurring in ϕ ∈ L P and Var ({ϕ 1 , . . . , ϕ k }) = k i=1 Var (ϕ i ); when X ⊆ P, we have Var (∃X.ϕ) = Var (ϕ) \ X.

A literal is a propositional variable or a negated one. When is a literal over x, its complementary literal ∼ is given by ∼ = ¬x if = x and ∼ = x if = ¬x, and we note var ( ) = x. A literal is pure in a CNF formula Σ when Σ contains no occurrence of ∼ . One also says that the corresponding variable var ( ) is pure in Σ. A term is a conjunction of literals. It is also viewed as the set of its literals when this is convenient. A clause is a disjunction of literals. When δ = m j=1 j is a clause, ∼δ denotes the term given by m j=1 ∼ j . A clause δ 1 is a subclause of a clause δ 2 when every literal of δ 1 is a literal of δ 2 . A CNF formula ϕ is a conjunction of clauses. It is also viewed as the set of its clauses when this is convenient. ϕ denotes the number of models of ϕ over Var (ϕ).

Given a subset X of P and a world ω, ω[X] is the term

x∈X|ω|=x x ∧ x∈X|ω|=¬x ¬x.
The conditioning of a CNF formula ϕ by a consistent term γ is the CNF formula ϕ | γ obtained from ϕ by removing each clause containing a literal of γ and by shortening the remaining clauses, removing from them the complementary literals of those of γ.

BCP denotes a Boolean Constraint Propagator [START_REF] Zhang | An efficient algorithm for unit propagation[END_REF][START_REF] Moskewicz | Chaff: Engineering an efficient SAT solver[END_REF], which is a key component of many solvers. BCP(Σ) returns the CNF formula Σ once simplified using unit propagation.

The primal graph of a CNF formula Σ is the (undirected) graph where vertices correspond to the variables of Σ and an edge connecting two variables exists whenever one can find a clause of Σ where both variables occur. Every connected component of this graph (i.e., a maximal subset of vertices which are pairwise connected by a path) corresponds to a subset of clauses of Σ, referred to as a connected component of the formula Σ.

A Recursive Algorithm for Projected Model Counting

Our projected model counter projMC computes ∃X.Σ where Σ is a CNF formula and X a set of propositional variables. Assuming Σ being in CNF is harmless since one can use Tseitin technique [START_REF] Tseitin | On the complexity of derivation in propositional calculus[END_REF] to associate in linear time with any propositional circuit a CNF formula having the same number of models.

Unlike the previous algorithms for projected model counting sketched in the introductive section, projMC is a recursive algorithm guided by a deterministic disjunctive form for Σ w.r.t. X. Such a form is a (disjunctively interpreted) set of formulae {ϕ 1 , . . . , ϕ k+1 } over Var (Σ) satisfying the following conditions:

• ∀i ∈ {1, . . . , k + 1}, Var (ϕ i ) ∩ X = ∅; • ∀i, j ∈ {1, . . . , k + 1}, if i = j then ϕ i ∧ ϕ j |= ⊥; • k+1 i=1 ϕ i ≡ . Because k+1 i=1 ϕ i is valid, we have ∃X.Σ ≡ (∃X.Σ) ∧ ( k+1 i=1 ϕ i ) ≡ k+1 i=1 (∃X.Σ)∧ϕ i ≡ k+1 i=1 ∃X.(Σ∧ϕ i ) since
no element of a deterministic disjunctive form for Σ w.r.t. X contains a variable of X. Furthermore, since the elements of a deterministic disjunctive form for Σ w.r.t. X are pairwise conflicting, we get that ∃X.Σ = k+1 i=1 (∃X.Σ) ∧ ϕ i , hence

∃X.Σ = k+1 i=1 ∃X.(Σ ∧ ϕ i ) . The set {Σ ∧ ϕ i | i ∈ {1, . . . , k + 1}} is referred to as the disjunctive decomposition associated with {ϕ 1 , . . . , ϕ k+1 }.
Technically speaking, such a notion of disjunctive decomposition can be related to several concepts considered in some previous works about SAT or #SAT. On the one hand, it can be viewed as a specific case of the notion of set of scattered formulae from a formula Σ (see [START_REF] Hyvärinen | A distribution method for solving SAT in grids[END_REF] for details), obtained by focusing on clauses/terms not containing any variable from X. However, the objective pursued in [START_REF] Hyvärinen | A distribution method for solving SAT in grids[END_REF] was quite distinct from our own one (in this paper, the decomposition was used as a distribution method for SAT solving in grids). On the other hand, when it consists of consistent formulae, a deterministic disjunctive form for Σ w.r.t. X forms a partition, just as the primes of an X-partition of Σ, used for generating an SDD representation of Σ (see (Darwiche for details). Nevertheless, the connection to SDD does not extend further: whenever Σ contains variables from X and from Var (Σ) \ X, the disjunctive decomposition associated with a deterministic disjunctive form is not a (X, Var (Σ) \ X)-decomposition of Σ: disjunctive decompositions do not aim to create formulae that do not share variables.

Clearly enough, generating a disjunctive decomposition {Σ ∧ ϕ i | i ∈ {1, . . . , k + 1}} associated with a deterministic disjunctive form for Σ w.r.t. X is computationally useful for computing ∃X.Σ only if the formulae Σ ∧ ϕ i are somewhat more simple than Σ. To ensure it and guarantee the termination of projMC, one does not compute any deterministic disjunctive form for Σ w.r.t. X but one induced by a model ω of Σ (if there is not such model, then ∃X.Σ is inconsistent and ∃X.Σ = 0). One starts by considering the

CNF formula Σ | ω[X] = k i=1 δ i , called the core ϕ 1 of the deterministic disjunctive form {ϕ 1 , . . . , ϕ k+1 } for Σ w.r.t. X induced by ω. By construc- tion, ϕ 1 = k i=1 δ i contains variables occurring in Var (Σ)
but not in X. Then we generate a (disjunctively interpreted) set of CNF formulae {ϕ 2 , . . . , ϕ k+1 } which is equivalent to the negation of ϕ 1 , by defining, for each i ∈ {1, . . . , k}, ϕ i+1 = ( i-1 j=1 δ j ) ∧ ∼δ i . By construction, {ϕ 1 , . . . , ϕ k+1 } satisfies the conditions of a deterministic disjunctive form for Σ w.r.t. X. Note also that ∃X.

(Σ ∧ ϕ 1 ) is equivalent to ϕ 1 . Indeed, ∃X.(Σ ∧ ϕ 1 ) is equivalent to (∃X.Σ) ∧ ϕ 1 since ϕ 1 does not contain any variable of X. Furthermore, since ω[X] ∧ Σ |= Σ, we have that ∃X.(ω[X] ∧ Σ) |= ∃X.Σ. But ∃X.(ω[X] ∧ Σ) is equivalent to Σ | ω[X]
, hence to ϕ 1 , so ϕ 1 |= ∃X.Σ, and as a consequence (∃X.Σ) ∧ ϕ 1 is equivalent to ϕ 1 . Accordingly, when computing the number of models of the disjunctive decomposition {Σ ∧ ϕ i | i ∈ {1, . . . , k + 1}} associated with {ϕ 1 , . . . , ϕ k+1 }, one replaces Σ ∧ ϕ 1 by ϕ 1 . Since Var (ϕ 1 ) ∩ X = ∅, one can take advantage of a "standard" model counter for computing ϕ 1 and no recursive call of projMC is needed (this is a base case for the recursion).

Our algorithm projMC also takes advantage of any conjunctive decomposition of its input Σ into disjoint connected components whenever such a decomposition exists. Indeed, whenever Σ can be split into two sets of clauses α and β not sharing any variable so that Σ ≡ α ∧ β, then the computation of ∃X.Σ can be achieved by computing ∃X.α and ∃X.β since ∃X.Σ ≡ ∃X.(α ∧ β) ≡ (∃X.α) ∧ (∃X.β). And since ∃X.α and ∃X.β do not share any variable, one can compute ∃X.Σ = ∃X.α × ∃X.β . As it is the case for the model counting problem, taking advantage of conjunctive decompositions proves to be very useful for the efficiency purpose.

Algorithm 1: projMC(Σ, X) input : a CNF formula Σ input : a set of variables X to be forgotten output: the number of models of ∃X.Σ over

Var (Σ) \ X 1 Σ ← BCP(Σ) 2 if Var (Σ) ∩ X = ∅ then return MC(Σ) 3 if cache(Σ) = nil then return cache(Σ) 4 comps ← connectedComponents(Σ) 5 if #(comps) = 1 then 6 cpt ← 1 7 foreach ϕ ∈ comps do 8 cpt ← cpt× projMC(ϕ, X) 9 else 10 ω ← sat(Σ) 11 cpt ← 0 12 if ω = ∅ then 13 dd ← DD(Σ, ω, X) 14 foreach ϕ ∈ dd do 15 cpt ← cpt+ projMC(ϕ, X) ×2 #(Var (dd)\(Var (ϕ)∪X)) 16 cache(Σ) ← cpt 17 return cpt
More in detail, Algorithm 1 provides the pseudo-code of the projected model counter projMC. The projected model counting of a given CNF formula Σ w.r.t. a set of variables X to be forgotten is achieved by calling projMC(Σ, X). At line 1, Σ is simplified using Boolean constraint propagation. At line 2, we consider the case when Σ does not contain any variable of X. In this case, there is no variable to be forgotten and it is enough to compute the number of models of Σ, using any model counter MC. This is a base case of our algorithm (no recursion takes place).

At line 3 one looks into a cache to check whether or not the current formula Σ has already been encountered during the search. The cache, initially empty, gathers pairs consisting of a CNF formula and the corresponding projected model count w.r.t. X. Each time Σ has already been cached, instead of re-computing ∃X.Σ from scratch, it is enough to return cache(Σ). In our implementation, the cache is residual and shared with the model counter MC.

At line 4, one partitions Σ into a set of CNF formulae that are pairwise variable-independent (i.e., two distinct elements of comps are built up from two disjoint sets of variables). connectedComponents is a "standard" procedure used in previous model counters. It is based on the search for the connected components of the primal graph of Σ and it returns a set comps of CNF formulae composed of clauses from Σ, so that every pair of distinct formulae from comps do not share any common variable.

At line 5, one tests how many connected components have been found in Σ. If there are more than one component, then at lines 6, 7, and 8, one recursively computes the projected model counts corresponding to each of them, and we store in cpt the product of the corresponding counts. For efficiency reasons, in our implementation, one uses a specific trick that it is not made explicit in the algorithm for the sake of readibility: systematically, one sets aside all the components forming a consistent term containing as many literals as possible. For instance, if the input Σ is equal to x 1 ∧ ¬x 2 ∧ (x 3 ∨ x 4 ), one sets aside the two components x 1 and ¬x 2 to keep only the component x 3 ∨ x 4 . Indeed, for a set of components forming a consistent term like {x 1 , ¬x 2 }, the corresponding projected model count is always equal to 1 (whatever the variables occurring in the term belongs to X or not). Hence projMC returns directly 1 in this case, without needing to consider the literals of the term independently in distinct recursive calls.

When only one component of Σ has been found, at line 10, one looks for a model ω of Σ over Var (Σ). One tests at line 12 whether such a model exists. If not (ω = ∅), then Σ is inconsistent, hence so is ∃X.Σ, and the model count is 0, the value of cpt initialized at line 11. Interestingly, the heuristic used by the solver sat tries to satisfy Σ by assigning in priority the variables from X. A valuable consequence of this choice is that it leads to a lazy handling of the clauses of Σ which contain a literal pure in Σ and such that var ( ) = x with x ∈ X. Indeed, when is pure in Σ, will be set to 1 by ω so that no clauses of Σ containing will belong to Σ | ω[X]. This does not invalidate the correctness of the approach since such clauses can be removed from Σ without changing its projected model count. Thus, while the "standard" pure literal rule (i.e., the one consisting in removing every clause of Σ containing a variable which is pure in Σ) cannot be applied safely (it does not preserve the number of models of its input in the general case), its restriction where only pure literals over X are considered is correct: let α (resp. β) be the subset of the clauses of Σ containing (resp. not containing ). We have ∃X.Σ ≡ ∃X.(∃{x}.(α ∧ β)). Since is pure in Σ, x does not occur in β. Hence ∃{x}.(α ∧ β) ≡ (∃{x}.α) ∧ β. Now, since every clause of α contains , ∃{x}.α is valid, therefore ∃X.Σ ≡ ∃X.β.

At line 13, one computes the disjunctive decomposition dd associated with the deterministic disjunctive form for Σ w.r.t. X induced by ω. At lines 14, and 15, one sums the projected model counts for the formulae belonging to dd (note that when the elements ϕ of dd do not contain the same set of variables, a preliminary normalization step -multiplying each count by 2 to the power of the number of variables occurring in dd but not in ϕ and not in X -before summing up, is necessary). Finally, at line 16, one adds Σ to the cache, associated with the corresponding projected model count cpt, and at line 17, one returns the value of cpt.

Algorithm 2: DD(Σ, ω, X) input : a CNF formula Σ input : a model ω of Σ over Var (Σ) input : a set of variables X to be forgotten output: a set dd of CNF formulae, the disjunctive decomposition associated with the deterministic disjunctive form for Σ w.r.t. X induced by ω

1 {δ 1 , . . . , δ k } ← BCP(Σ | ω[X]) 2 dd ← { k i=1 δ i } 3 foreach δ j ∈ {δ 1 , . . . , δ k } do 4 dd ← dd ∪ {Σ ∧ ( j-1 l=1 δ l ) ∧ ∼δ j } 5 return dd
Algorithm 2 provides the pseudo-code of the program which generates the disjunctive decomposition associated with the deterministic disjunctive form of Σ w.r.t. X induced by the model ω of Σ used for guiding the search. At line 1, Σ is first conditioned by the consistent term ω[X]. This means that every clause of Σ containing a literal belonging to ω[X] is removed from Σ, and in the remaining clauses, every literal over X such that ∼ is a literal of ω[X] is removed. Finally, Boolean constraint propagation is applied to Σ | ω[X] in order to simplify it further (if possible). Clearly, no variable of X occurs in the resulting (conjunctively interpreted) set of clauses {δ 1 , . . . , δ k }, which is the core of the deterministic disjunctive form for Σ w.r.t. X induced by ω that is computed. At line 2, we first initialize the disjunctive decomposition dd as the singleton containing the core. At lines 3 and 4, we add to dd k CNF formulae since the core contains k clauses. At line 4, the clauses of Σ subsumed by the clauses δ l are removed (this is not detailed in the pseudocode for the sake of readability). By construction, the formulae of dd are pairwise inconsistent. Furthermore, every δ j of the core is a subclause of a clause of Σ since the core is obtained by conditioning Σ using a consistent term. Accordingly, in our implementation, when δ j is equal to a clause of Σ, δ j is not taken into consideration within the loop (indeed, in this case, Σ ∧ δ j is equivalent to Σ and Σ ∧ ∼δ j is inconsistent, so that its contribution to the total model count will be equal to 0). Finally, at line 5, one returns the disjunctive decomposition dd which has been computed.

An Example.

Here is an example illustrating how projMC works

. Let Σ = (x 1 ∨ x 2 )∧ (¬x 2 ∨ x 3 ∨ x 4 )∧ (¬x 3 ∨ x 5 ). Let X = {x 2 , x 3 }. The formula ∃X.Σ is equivalent to x 1 ∨ x 4 ∨ x 5 , so that ∃X.Σ = 7.
When run on Σ and X, the first instructions of projMC have no effect (applying BCP does not change Σ, and Σ has a unique connected component). Suppose that the model ω of Σ setting every variable to 1 has been found at line 10. Then the core Σ | ω[X] of the deterministic disjunctive form for Σ w.r.t. X induced by ω will be equal to x 5 . As a consequence, the other formula belonging to the disjunctive decomposition associated with this deterministic disjunctive form will be Σ ∧ ¬x 5 .

The recursive call of projMC on the core x 5 and X will lead to calling MC on x 5 as expected (since no variable of X occurs in the core). Then MC returns 1, and finally the recursive call of projMC on x 5 returns 1 × 2 2 = 4 since the two variables x 1 , x 4 belong to the set of variables of dd but not to the set of variables of the associated core (this normalization step is achieved at line 15).

The recursive call of projMC on Σ ∧ ¬x 5 and X leads first to simplify Σ ∧ ¬x 5 using BCP, so that the formula ¬x 5 ∧ (x 1 ∨ x 2 ) ∧ (¬x 2 ∨ x 4 ) ∧ ¬x 3 is got. Since the two components ¬x 5 and ¬x 3 form together a consistent term, only one component actually needs to be considered, namely

(x 1 ∨ x 2 ) ∧ (¬x 2 ∨ x 4 ).
So, at that step, projMC is called on (x 1 ∨x 2 ) ∧ (¬x 2 ∨x 4 ) and X. Suppose again that the model ω of Σ setting every variable to 1 has been found. Then the resulting core will be equal to x 4 , and the disjunctive decomposition will be {x 4 , (x 1 ∨ x 2 ) ∧ (¬x 2 ∨ x 4 ) ∧ ¬x 4 }. Since ¬x 4 does not contain a variable of X, at the next recursive call to projMC, MC is used to compute its model count, equal to 1, and finally the recursive call of projMC on x 4 returns 1 × 2 1 = 2 since the variable x 1 belongs to the set of variables of the disjunctive decomposition but not to the set of variables of the associated core. The recursive call of projMC on (x 1 ∨x 2 ) ∧ (¬x 2 ∨x 4 ) ∧ ¬x 4 and X leads first to simplify (using BCP) the input into x 1 ∧ ¬x 2 ∧ ¬x 4 , which is a consistent term. Hence it has only 1 model. Thus one obtains that ∃X.((

x 1 ∨ x 2 ) ∧ (¬x 2 ∨ x 4 )) = 2 + 1 = 3.
Finally the previously computed counts are summed up. One thus gets 4 + 3 = 7 models, as expected.

Interestingly, it can be observed that projMC handles adequately the cases when X = ∅ or X = Var (Σ), in the sense that it does not waste too much time in many recursive calls for any of those two "extreme" situations. Indeed, when X = ∅, projMC mainly boils down to calling a "standard" model counter MC (line 2), as expected. When X = Var (Σ), if Σ is unsatisfiable, then it will be detected as such during the first call to projMC (line 12) and a count of 0 will be returned. In the remaining case, a model ω of Σ will be found. The core of the deterministic disjunctive form for Σ w.r.t. X induced by ω will be equal to the empty set of clauses since Σ | ω[Var (Σ)] is valid when ω is a model of Σ. Hence the disjunctive decomposition associated with this deterministic disjunctive form will consist only of this core. Because this core contains no variable, the next recursive call to projMC (i.e., the one with the core as an operand) will mainly consist in calling the model counter MC (line 2) on it, and MC will return 1 in this case.

Finally, one can prove that our algorithm projMC actually does the job for which it has been designed: Proposition 1 Algorithm 1 is correct and terminates. Proof: The correctness of projMC (i.e., the fact that the result provided is equal to ∃X.Σ on inputs Σ and X) comes from the fact that each rule used in the algorithm is sound w.r.t. the projected model counting task, as explained previously. The key equalities are ∃X.Σ = k+1 i=1 ∃X.(Σ ∧ ϕ i ) for any deterministic disjunctive form {ϕ 1 , . . . , ϕ k+1 } for Σ w.r.t. X, and ∃X.(α ∧ β) = ∃X.α × ∃X.β when Var (α) ∩ Var (β) = ∅.

The termination of projMC comes from the fact that each time a deterministic disjunctive form for Σ w.r.t. X is computed, its core does not contain any variable of X, so that the recursive call to projMC concerning it will lead to the base case of the recursion (line 2). As to the other disjoints Σ ∧ ϕ i of the corresponding disjunctive decomposition, by construction, every ϕ i contains the negation of a subclause δ i-1 of Σ. Hence, at the next call to projMC concerning this disjoint, the literals of the term ∼δ i-1 will be assigned and the corresponding variables will be removed from the input using Boolean constraint propagation (line 1). Thus the number of variables of the input strictly diminishes at each step and this ensures the termination of the algorithm.

Note that the detection of disjoint components (lines 4 to 9 in Algorithm 1) coud be frozen in projMC without questioning the correctness and the termination of this algorithm (however, it has a significant impact on the efficiency of the computation on some instances). Similarly, the use of a cache has no impact on the correctness or the termination of the algorithm, so that the instructions at lines 3 and 16 could be frozen as well (but again using a cache proves to be computationally useful in many cases).

Empirical Evaluation

In order to evaluate the benefits offered by projMC, we performed some experiments. The empirical protocol we followed is precisely the same as the one considered in [START_REF] Aziz | #∃SAT: Projected model counting[END_REF]. Thus we have considered 260 instances coming from three data sets. The first data set consists of 100 instances, based on random 3-CNF formulae, where the number of variables is set to 100 and the number of clauses is varied. Clause-to-variable ratios of 1, 1.5, 2, 3, and 4 have been considered. We let also the number of variables of X to vary (the elements of X are chosen uniformly at random). The second data set consists of 60 instances, corresponding to random Boolean circuits based on 30 variables. Those circuits are generated as follows. One keeps a set containing at start the 30 variables, and as long as the set is not a singleton, we randomly select an operator o (AND, OR, NOT), pick up operands V for o in the set at random, create a new variable v, add the gate o ↔ o(V ) to the circuit, and put v back in the set. The process is repeated c times, with c equals to 1, 5, or 10. Finally, the third data set consists of 100 instances generated from five classical planning problems (depots, driver, rovers, logistics, and storage) considered under varying planning horizons. For each problem and value of the horizon, two variants are considered, one with the goal state fixed and one where the goal is relaxed to be any viable goal. For the first variant, the projected model count to be computed represents the number of initial states the given plan can achieve the goal from. For the second variant, it gives the number of initial states plus all goal configurations that the given plan works for.

For each instance, we measured the time (in seconds) required by projMC to achieve the projected model counting job. In the experiments, the model counter MC used in projMC is the top-down compilation-based model counter D4 described in [START_REF] Lagniez | An improved decision-DNNF compiler[END_REF]. For the sake of comparison, we have also run the previous projected model counters dSharp P , #clasp, and d2c on the same instances (those solvers are available from people.eng.unimelb.edu.au/ pstuckey/countexists) and measured the corresponding computation times. In addition, we have also compared projMC with P , which is the same algorithm as dSharp P , but using D4 as the underlying model counter instead of dSharp. All the experiments have been conducted on a cluster of Intel Xeon E5-2643 (3.30 GHz) quad core processors with 32 GiB RAM. The kernel used was CentOS 7, Linux version 3.10.0-514.16.1.el7.x86 64. The compiler used was gcc version 5.3.1. Hyperthreading was disabled, and no memory share between cores was allowed. A timeout of 600s and a memory-out of 7.6 GiB has been considered for each instance.

The results are reported on the scatter plots given in Figure 1. Each dot represents an instance; the time (in seconds) needed to solve it using the projected model counter corresponding to the x-axis (resp. y-axis), is given by its xcoordinate (resp. y-coordinate). Logarithmic scales are used for both coordinates. In part (a) (resp. (b), (c), (d)) of the figure, the x-axis corresponds to dSharp P (resp. #clasp, d2c, D4 P ). The y-axis corresponds to projMC in each part of the figure.

The four scatter plots in Figure 1 clearly show that for a great majority of instances the time needed by projMC to count the number of projected models is smaller (and often significantly smaller) than the corresponding computation times when the other projected model counters are used. This is especially the case when the "trivial" instances (i.e., those solved with a second or alike) are neglected. Notwithstanding those instances, it is interesting to observe that projMC appears at least as efficient as any of the other projected model counters for all the instances from the random and the planning data sets.

The cactus plot in Figure 2 gives for dSharp P , #clasp, d2c, D4 P , and projMC the number of instances solved in a given amount of time. Clearly enough, projMC outperforms the previous projected model counters: when the "trivial" instances have been discarded, projMC typically solves more instances than any of them in any given amount of time. Especially, some significant benefits in terms of the number of instances solved have been obtained. Table 2 shows that projMC was able to solve a significant number of instances that were out of reach for the other projected model counters, given the time limit under consideration. That mentioned, the virtual best solver for our experiments would solve 211 instances, which is slightly above 192. This coheres with the results reported in Figure 1 (d), showing that for the circuit instances, D4 P typically challenges projMC.

Conclusion and Perspectives

We have presented a new algorithm, projMC, for computing the number of models ∃X.Σ of a propositional formula Σ after eliminating from it a given set X of variables. Unlike previous algorithms, projMC takes advantage of a disjunctive decomposition scheme of ∃X.Σ for computing ∃X.Σ . It also looks for disjoint components in its input for improving the computation. Our experiments have shown that projMC can be significantly more efficient than the existing algorithms dSharp P , #clasp, and d2c for projected model counting. Empirically, projMC also proved better than D4 P on many instances, showing that the improved performance of projMC is not solely due to the the fact that it is "powered" by D4.

A first perspective for further research consists in turning our projected model counter into a compiler generating a d-DNNF representation from a CNF formula containing some existentially quantified variables. Provided that the underlying model counter MC is replaced by a d-DNNF compiler (like C2D [START_REF] Darwiche | A compiler for deterministic decomposable negation normal form[END_REF][START_REF] Darwiche | New advances in compiling CNF into decomposable negation normal form[END_REF], dSharp (Muise et al. 2012) or D4 (Lagniez and Marquis 2017)), the changes to be done mainly consist in modifying the instructions at lines 14 and 15 of Algorithm 1 to generate a deterministic OR node instead of making a summation. In such a compiler, when a model of Σ is generated (i.e., at a step corresponding to line 10 of Algorithm 1), one could look for an assignment maximizing the number of clauses which are satisfied by some existentially quantified literals of the model, so as to get a deterministic disjunctive form which contains as few elements as possible (hence a deterministic OR node with as few children as possible). In fact, one already tested this approach within projMC but the benefits achieved are not that significant in this case -the time spent in the maximisation processes can be quite large. However, things can be different when the objective is to generate a compiled representation since, in such a setting, one is typically ready to spend more off-line time in the compilation step, provided that the size of the associated compiled form is significantly smaller. We plan to make some experiments in this direction to determine whether this approach could prove useful for generating more succinct compiled representations.

A second perspective will consist in taking advantage of the two programs B and E for gate detection and replacement within CNF formulae, used as the key components of the preprocessor for model counting reported in [START_REF] Lagniez | Improving model counting by leveraging definability[END_REF]. Indeed, B and E could be exploited as additional inprocessing filtering techniques in projMC. It would be interesting to determine whether this could be computationally useful, especially for solving circuit instances where, by construction, many gates can be found.

A last perspective will consist in evaluating projMC and the other projected model counters on other benchmarks, especially those reported in the repository available from https://github.com/ dfremont/counting-benchmarks/tree/ master/benchmarks/projection. 1 1 We would like to thank an anonymous reviewer for pointing out this dataset.

Figure 1 :

 1 Figure 1: Comparing projMC with dSharp P , #clasp, d2c, and D4 P . The coordinates correspond to computation times in seconds. Logarithmic scales are used.

Figure 2 :

 2 Figure 2: Number of instances solved by dSharp P , #clasp, d2c, D4 P , and projMC in a given amount of time.

Table 1 :

 1 Thus, Table1makes precise for each projected model counter under consideration the number of instances (over 260) which have been solved within the time limit of 600s. It can be observed that projMC has been able to solve many more instances than the other projected model counters. Number of instances solved within the time limit depending on the projected model counter used.

	projected model counter # of instances solved
	dSharp P	115
	#clasp	94
	d2c	71
	D4 P	140
	projMC	192
	Table 2 reports for each projected model counter un-
	der consideration the number of instances which have been
	solved by it, and only by it.
	projected model counter # of instances uniquely solved
	dSharp P	0
	#clasp	1
	d2c	0
	D4 P	1
	projMC	44

Table 2 :

 2 Number of instances uniquely solved within the time limit depending on the projected model counter used.