--- title: "A Unifying Formal Approach to Importance Values in Boolean Functions" authors: - "Hans Harder" - "Simon Jantsch" - "Christel Baier" - "Clemens Dubslaff" doi: "10.24963/ijcai.2023/304" url: "https://ijcai.org/proceedings/2023/304" pdf: "https://ijcai.org/proceedings/2023/0304.pdf" venue: "Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence" year: 2023 pages: "2728-2737" track: "Main Track" keywords: - "Constraint Satisfaction and Optimization: CSO: Satisfiabilty" - "AI Ethics, Trust, Fairness: ETF: Explainability and interpretability" - "Game Theory and Economic Paradigms: GTEP: Cooperative games" --- # A Unifying Formal Approach to Importance Values in Boolean Functions Hans Harder, Simon Jantsch, Christel Baier, Clemens Dubslaff *Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence*, pages 2728-2737. DOI: [10.24963/ijcai.2023/304](https://doi.org/10.24963/ijcai.2023/304) ## Abstract Boolean functions and their representation through logics, circuits, machine learning classifiers, or binary decision diagrams (BDDs) play a central role in the design and analysis of computing systems. Quantifying the relative impact of variables on the truth value by means of importance values can provide useful insights to steer system design and debugging. In this paper, we introduce a uniform framework for reasoning about such values, relying on a generic notion of importance value functions (IVFs). The class of IVFs is defined by axioms motivated from several notions of importance values introduced in the literature, including Ben-Or and Linial’s influence and Chockler, Halpern, and Kupferman’s notion of responsibility and blame. We establish a connection between IVFs and game-theoretic concepts such as Shapley and Banzhaf values, both of which measure the impact of players on outcomes in cooperative games. Exploiting BDD-based symbolic methods and projected model counting, we devise and evaluate practical computation schemes for IVFs. ## Full text ## 1 Introduction Boolean functions arise in many areas of computer science and mathematics, e.g., in circuit design, formal logics, coding theory, artificial intelligence, machine learning, and system analysis [Crama and Hammer, 2011a; O'Donnell, 2014]. When modeling and analyzing systems through Boolean functions, many design decisions are affected by the relevance of variables for the outcome of the function. Examples include noise-reduction components for important input variables to increase reliability of circuits, prioritizing important variables in decision-making of protocols, or the order of variables in BDDs [Bryant, 1992; Bartlett and Andrews, 2001]. Many ideas to quantify such notions of importance of variables in Boolean functions have since been considered in the literature. To mention a few, influence [Ben-Or and Linial, 1985] is used to determine power of actors in voting schemes, [Hammer et al., 2000] devised measures based on how constant a function becomes depending on variable assignments, blame [Chockler and Halpern, 2004] quantifies the average responsibility [Chockler et al., 2008] of input variables on the outcome of circuits or on causal reasoning, and the Jeroslow-Wang value [Jeroslow and Wang, 1990] quantifies importance of variables in CNFs to derive splitting rules for SAT-solvers [Hooker and Vinay, 1995]. Closely related are notions of impact in cooperative games, e.g., through the Shapley value [Shapley, 1953] or the Banzhaf value [Banzhaf, 1965]. Although some of the aforementioned concepts are of quite different nature and serve different purposes, they share some common ideas. This raises the question of what characteristics importance values have and how the notions of the literature relate. The motivation of this paper is to advance the understanding of importance values, independent of concrete applications. For this purpose, we introduce a generic axiomatic framework that constitutes the class of importance value functions (IVFs). Our axioms are motivated by properties one would intuitively expect from IVFs, e.g., that independent variables have no importance or that permutations do not change importance values. We show basic relationships within and between IVFs and provide new insights for existing and new importance measures. By connecting Boolean functions and cooperative games through cooperative game mappings (CGMs) and using Shapley and Banzhaf values, we show how to generically derive new IVFs . All aforementioned notions of importance values from the literature satisfy our IVF axioms, showing that we provide a unifying framework for all these notions, including CGM-derived ones. Most notions of importance are known to be computationally hard, e.g., computing influence or the Shapley value is #P-complete [Traxler, 2009; Faigle and Kern, 1992; Deng and Papadimitriou, 1994]. We address computational aspects by devising practical computation schemes for IVFs using projected model counting [Aziz et al., 2015] and BDDs. Contributions and outline. In summary, our main contribution is an axiomatic definition of IVFs for variables in Boolean functions (Section 3), covering notions of importance from the literature (Sections 4.1 and 4.2). Moreover, we derive novel IVFs by linking Boolean functions with cooperative games and related values (Section 4.3). Finally, we provide practical computation schemes for IVFs (Section 5). Supplemental material. All proofs can be found in an extended version at https://arxiv.org/abs/2305.08103. An implementation of the computing schemes for IVFs can be found at https://github.com/graps1/impmeas. ## 2 Preliminaries Let X = {x, y, z, . . . } be a finite set of n = |X| variables, which we assume to be fixed throughout the paper. Assignments. An assignment over U ⊆ X is a function u: U → {0, 1}, written in the form u = x/0; y/1; . . . . We denote assignments by bold lower-case letters and their domains by corresponding upper-case letters. If u and v have disjoint domains, we write their concatenation as w = u; v with W = V ∪ U and w(x) = u(x) if x ∈ U and w(x) = v(x) if x ∈ V . The restriction of u to a domain S ⊆ U is denoted by uS . For a permutation σ of X, we define σu as the assignment over σ(U) with (σu)(x) = u(σ-1 (x)). Boolean functions. We call f, g, h, · · · : {0, 1}X → {0, 1} Boolean functions, collected in a set B(X). We write g = x if g is the indicator function of x, and we write g for negation, f ∨ g for disjunction, fg for conjunction and f ⊕ g for exclusive disjunction. The cofactor of f w.r.t. an assignment v is the function fv that always sets variables in V to the value given by v, and is defined as fv(u) = f(v;uU\V ). The Shannon decomposition of f w.r.t. variable x is a decomposition rule stating that f = xfx/1 ∨ xfx/0 holds, where fx/1 and fx/0 are the positive and negative cofactor of f w.r.t. x. For a Boolean function f, variable x, and Boolean function or variable s, let f[x/s] = sfx/1 ∨ sfx/0 be the function that replaces x by s. For example, if f = y∨xz, then fx/1 = y∨z and fx/0 = y. Moreover, for s = x1x2, we have For ∼ ∈ {≤,≥,=}, we write f ∼ g if f(u) ∼ g(u) is true for all assignments. We collect the variables that f depends on in the set dep(f) = {x ∈ X : fx/1 ̸= fx/0}. If v is an assignment with dep(f) ⊆ V , then f(v) denotes the only possible value that fv can take. We say that f is monotone in x if fx/1 ≥ fx/0, and call f monotone if f is monotone in all of its variables. Furthermore, f is the dual of g if f(u) = g(u), where u is the variable-wise negation of u. We call f symmetric if f = σf for all permutations σ of X, where σf(u) = f(σ-1u). Expectations. We denote the expectation of f w.r.t. the uniform distribution over D by Ed∈D[f(d)] for f : D → R. We only consider cases where D is finite, so If the domain of f is clear, we simply write E[f]. For f ∈ B(X), E[f] is the fraction of satisfying assignments of f. Modular decompositions. We introduce a notion of modularity to capture independence of subfunctions as common in the theory of Boolean functions and related fields [Ashenhurst, 1957; Birnbaum and Esary, 1965; Shapley, 1967; Bioch, 2010]. Intuitively, f is modular in g if f treats g like a subfunction and otherwise ignores all variables that g depends on. We define modularity in terms of a template function ℓ in which g is represented by a variable x: Definition 1. Let f, g ∈ B(X). We call f modular in g if g is not constant and there is ℓ ∈ B(X) and x ∈ X such that dep(ℓ) ∩ dep(g) = ∅ and f = ℓ[x/g]. If ℓ is monotone in x, then f is monotonically modular in g. If f is modular in g with ℓ and x as above, then f(u) = ℓ(w), where w is defined for y ∈ X as Thus, the value computed by g is assigned to x and then used by ℓ, which otherwise is not influenced by the variables that g depends on. For example, f = x1 ∨z1z2x2 is modular in g = z1z2 since f can be obtained by replacing x in ℓ = x1 ∨ xx2 by g. Note that dep(ℓ) = {x, x1, x2} and dep(g) = {z1, z2} are disjoint. This property is crucial, since it ensures f and g are coupled through variable x only. If f is modular in g, then the cofactors ℓx/1 and ℓx/0 must be unique since g is not constant. Hence, we can define the cofactors of f w.r.t. g as fg/1 = ℓx/1 and fg/0 = ℓx/0. The instantiation is reversed by setting f [g/x] = xfg/1 ∨ xfg/0. Boolean derivatives. We frequently rely on the derivative of a Boolean function f w.r.t. variable x, which encodes the undirected change of f w.r.t. x. For example, f = x ∨ y has the derivative Dxf = y, with the intuition that x can only have an impact if y is set to zero. Furthermore, if f is modular in g, we define the derivative of f w.r.t. g as Dgf = fg/1 ⊕ fg/0. Given this, we obtain the following lemma corresponding to the chain rule known in calculus: ## 3 Importance Value Functions In this section, we devise axiomatic properties that should be fulfilled by every reasonable importance attribution scheme. For a Boolean function f and a variable x, we quantify the importance of x in f by a number Ix(f) ∈ R, computed by some value function I. Not every value makes intutive sense when interpreted as the "importance" of x, so we need to pose certain restrictions on I. We argue that I should be bounded, with 1 marking the highest and 0 the lowest importance; that functions which are independent of a variable should rate these variables the lowest importance (e.g., Ix(f) = 0 if f = y ∨ z); that functions which depend on one variable only should rate these variables the highest importance (e.g., Ix(f) = 1 for f = x); that neither variable names nor polarities should play a role in determining their importance (e.g., Ix(xz) = Iz(xz), cf. [Slepian, 1953; Golomb, 1959]): Definition 2 (IVF). A value function is a mapping of the form I: X×B(X) → R with (x, f) ↦→ Ix(f). An importance value function (IVF) is a value function I where for all x, y ∈ X, permutations σ : X → X, and f, g, h ∈ B(X): BOUND, DUM for "dummy", DIC for "dictator" and TYPE for "type invariance" were discussed above. MODEC (for "modular encapsulation consistency") is the only property that allows the inference of non-trivial importance inequalities in different functions. Let us explain its intuition. We say that f encapsulates h on g if these functions satisfy (i) and (ii) fromMODEC. Intuitively, together with (i), condition (ii) states that if one can control the output of g, it is both easier to satisfy f than h (using fg/1 ≥ hg/1) and to falsify f than h (using hg/0 ≥ fg/0). We argue in MODEC that if f encapsulates h on g, then g's impact on f is higher than on h, and thus, the importance of variables in dep(g) (cf. (iii)) should be also higher w.r.t. f than w.r.t. h. Example. Let f = x1x2 ∨ x3x4x5, h = x3x4 ∨ x1x2x5, and I be an IVF. Then f encapsulates h on g = x1x2, since We then get Ix1 (f) ≥ Ix1 (h) by application of MODEC. Swapping x1 with x3 and x2 with x4, we obtain a permutation σ such that h = σf. By TYPE, we derive Ix1 (h) = Ix3 (f). Using TYPE on the other variables yields Together with TYPE, MODEC implies the Winder preorder, which is similar in spirit (see [Hammer et al., 2000]). However, MODEC generalizes to modular decompositions and allows inferring importance inequalities w.r.t. to different functions. Biased and unbiased. We say that an IVF is unbiased if Ix(g) = Ix(g) holds for all Boolean functions g and variables x. That is, unbiased IVFs measure the impact of variables without any preference for one particular function outcome, while biased ones quantify the impact to enforce a function to return one or zero. Biased IVFs can, e.g., be useful when the task is to assign responsibility values for the violation of a specification. ## 3.1 Further Properties We defined IVFs following a conservative approach, collecting minimal requirements on IVFs. Further additional properties can improve on the predictability and robustness of IVFs. Definition 3. A value function I is called - rank preserving, if for all f, g ∈ B(X) such that f is modular in g and x, y ∈ dep(g): - chain-rule decomposable, if for all f, g ∈ B(X) such that f is modular in g and x ∈ dep(g): - where Ig(f) = Ixg (f[g/xg]) for some xg ̸∈ dep(f), - and derivative dependent, if for all f, g ∈ B(X), x ∈ X: We also consider weak variants of rank preserving and chainrule decomposable where f ranges only over functions that are monotonically modular in g. Rank preservation. Rank preservation states that the relation between two variables should not change if the function is embedded somewhere else. This can be desired, e.g., during a modeling process in which distinct Boolean functions are composed or fresh variables added, where rank preserving IVFs maintain the relative importance order of variables. We see this as a useful but optional property of IVFs since an embedding could change some parameters of a function that might be relevant for the relationship of both variables. For example, if f = gz with z ̸∈ dep(g), then the relative number of satisfying assignments is halved compared to g. If x is more important than y in g but highly relies on g taking value one, it might be that this relationship is reversed for f (cf. example given in Section 4.1). Chain-rule decomposability. If an IVF is chain-rule decomposable, then the importance of a variable in a module is the product of (i) its importance w.r.t. the module and (ii) the importance of the module w.r.t. the function. Many values studied in this paper satisfy this property (Section 4). Example. Let f = x1 ⊕ · · · ⊕ xm, and let I be a chain-rule decomposable IVFs with Ix(x ⊕ y) = α. Since f is modular in g = x1 ⊕ · · · ⊕ xm-1, and g modular in x1 ⊕ · · · ⊕ xm-2, etc., we can apply the chain-rule property iteratively to get Derivative dependence. Derivative dependence states that an IVF should quantify the change a variable induces on a Boolean function. It can be used to derive, e.g., the inequality Ix1 (x1 ⊕ x2x3) ≥ Ix1 (x2 ⊕ x1x3), which is not possible solely using MODEC since x1 ⊕ x2x3 is neither monotone in x1 nor in x2. If a value function I (that is not necessarily an IVF) is derivative dependent, then this has some interesting implications. First, I is unbiased and satisfies MODEC. Second, if I is weakly chain-rule decomposable (weakly rank preserving), then it is also chain-rule decomposable (rank preserving). Finally, if I satisfies DIC and DUM, then it is also bounded by zero and one. As a consequence, if I is derivative dependent and satisfies DIC, DUM, and TYPE, then I is an IVF. ## 3.2 Induced Relations In this section, we will establish foundational relations between IVFs. Recall that f is a threshold function if where {wx}x∈X ⊆ R is a set of weights and δ∈R a threshold. Theorem 1. Let I be an IVF, f, g, h∈B(X), x, y∈X. Then: - (1) If f is symmetric, then Ix(f) = Iy(f). - (2) If I is unbiased and f is dual to g, then Ix(f) = Ix(g). - (3) If f is a threshold function with weights {wx}x∈X ⊆ R, then |wx| ≥ |wy| implies Ix(f) ≥ Iy(f). - (4) If f is monotonically modular in g and x ∈ dep(g), then Ix(g) ≥ Ix(f ). - (5) If I is derivative dependent and x ̸∈ dep(g), then Ix(h ⊕ g) = Ix(h). - (6) If I is (weakly) chain-rule decomposable, then it is (weakly) rank preserving. For the case of threshold functions, Theorem 1 shows in (3) that any IVF will rank variables according to their absolute weights. In (4), it is stated that the if a function is monotonically embedded somewhere, the importance of variables in that function can only decrease, e.g., Ix(xy) ≥ Ix(xyz). Moreover, in (5), if derivative dependence is satisfied, ⊕- parts without the variable can be dropped. As a consequence, Ix(f) = 1 whenever f is a parity function and x ∈ dep(f). ## 4 Instances of Importance Value Functions In this section, we show that IVFs can be instantiated with several notions for importance values from the literature and thus provide a unifying framework. ## 4.1 Blame Chockler, Halpern, and Kupferman's (CHK) notions of responsibility [Chockler et al., 2008] and blame [Chockler and Halpern, 2004] measure the importance of x in f through the number of variables that have to be flipped in an assignment u until x becomes critical, i.e., "flipping" x changes the outcome of f to its complement. Towards a formalization, let denote the assignment that flips variables in S. We now rely on the following notion of critical set: Definition 4 (Critical sets). A critical set of x ∈ X in f ∈ B(X) under assignment u over X is a set S ⊆ X\{x} where We define scsux (f) as the size of the smallest critical set, and set scsux (f) = ∞ if there is no such critical set. Example. The set S = {y} is critical for x in f = x∨y under u = x/1; y/1. It is also the smallest critical set. On the other hand, there is no critical set if u = x/0; y/1. The responsibility of x for f under u is inversely related to scsux (f). Using the following notion of a share function, we generalize the original notion of responsibility [Chockler et al., 2008]: Definition 5 (Share function). Call ρ : N∪{∞} → R a share function if (i) ρ is monotonically decreasing, (ii) ρ(∞) = limn→∞ ρ(n) = 0, and (iii) ρ(0) = 1. In particular, we consider three instances of share functions: - ρexp(k) = 1/2k , - ρfrac(k) = 1/(k+1), - ρstep(k) = 1 for k = 0 and ρ(k) = 0 otherwise. Given a share function ρ, the responsibility of x for f under u is defined as ρ(scsux (f)). Note that ρfrac(scsux (f)) implements the classical notion of responsibility [Chockler et al., 2008]. While responsibility corresponds to the size of the smallest critical set in a fixed assignment, CHK's blame [Chockler et al., 2008] is a global perspective and fits our notion of value function. It is the expected value of the responsibility (we restrict ourselves to uniform distributions): Definition 6 (Blame). For a share function ρ, we define the ρblame as value function Bρ where for any x ∈ X, f ∈ B(X): Example. Let f = x∨y. To compute the importance of x we can count the number of times scsux (f) = 0, 1, 2, . . . ,∞ occurs if u ranges over the assignments for {x, y}: scsux (f) = ∞ happens once, scsux (f) = 0 happens twice, and scsux (f) = 1 occurs once. Thus, Bρx (f ) = 1/4·ρ(∞)+1/2·ρ(0)+1/4·ρ(1), which is 5/8 for ρ = ρexp. Independent of ρ, the blame is always an IVF: Theorem 2. Bρ is an unbiased IVF for any share function ρ. In full generality, the blame violates the optional properties for IVFs (see Section 3.1). For example, if ρ ̸= ρstep, then the ρ-blame is neither chain-rule decomposable nor derivative dependent, and one can find counterexamples for the rankpreservation property for ρfrac and ρexp: Proposition 1. Let ρ be a share function. Then the following statements are equivalent: - (i) Bρ is weakly chain-rule decomposable, - (ii) Bρ is derivative dependent, and - (iii) ρ = ρstep. Further, neither Bρfrac nor Bρexp are weakly rank preserving. To give an example for the reason why the ρfrac-blame is not weakly rank preserving, consider g = x1x0x2∨x1x0∨x3 and f = g ∨ z. Note that f is clearly monotonically modular in g - only z is added as fresh variable. Nevertheless, the order of x0 and x3 changes: Intuitively, this is because by CHK's definition of critical sets: for all Boolean functions h, variables x and assignments u, Hence, whenever an assignment u satisfies the premise for x in h, the responsibility of x for h under u will be zero. For x3, this is more frequently the case in g than in f (19% vs. 34% of all assignments). On the other hand, there is always a critical set for x0 in both f and g. Partly for this reason, the importance of x3 decreases more than x0 when switching from g to f. ## Modified Blame We modify the definition of critical sets in order to derive a modified blame that satisfies more optional properties for a wider class of share functions. For a Boolean function f, an assignment u over X and a variable x, the modified scs is defined as the size mscsux (f) of the smallest set S ⊆ X \ {x} that satisfies If there is no such set, we set mscsux (f) = ∞. Example. The condition for critical sets is relaxed, hence mscsux (f) provides a lower bound for scsux (f). Let for example f = x ∨ y and u = x/0; y/1. Then The definitions for responsibility and blame are analogous for the modified version, replacing scs by mscs. We denote by MBρ the modified ρ-blame, which is (in contrast to Bρ ) always derivative dependent and even chain-rule decomposable if ρ is an exponential- or stepping-function: Theorem 3. MBρ is an unbiased, derivative-dependent IVF for any share function ρ. If there is 0 ≤ λ < 1 so that ρ(k) = λk for all k ≥ 1, thenMBρ is chain-rule decomposable. ## 4.2 Influence The influence [Ben-Or and Linial, 1985; Kahn et al., 1988; O'Donnell, 2014] is a popular importance measure, defined as the probability that flipping the variable changes the function's outcome for uniformly distributed assignments: Definition 7. The influence is the value function I defined by Ix(f) = E[Dxf] for all f ∈ B(X) and variables x ∈ X. It turns out that the influence is a special case of blame: Since ρstep(k) = 0k for k ≥ 1, Proposition 2 and Theorem 3 show that the influence is a derivative-dependent, rankpreserving, and chain-rule decomposable IVF. ## Characterizing the Influence Call a value function I cofactor-additive if for all Boolean functions f and variables x ̸= z: Using this notion, we axiomatically characterize the influence as follows. Theorem 4. A value function I satisfies DIC, DUM, and cofactor-additivity if and only if I = I. Remark. A relaxed version of cofactor-additivity assumes the existence of αz, βz ∈ R for z ∈ X such that for all x ̸= z: This, together with the assumption that I satisfies TYPE, DUM and DIC, implies αz = βz = 1/2. Hence, another characterization of the influence consists of TYPE, DUM, DIC, and relaxed cofactor-additivity. Moreover, we give a syntactic characterization of the influence by a comparison to the two-sided Jeroslow-Wang heuristic used for SAT-solving [Jeroslow and Wang, 1990; Hooker and Vinay, 1995; Marques-Silva, 1999]. This value is defined for families of sets of literals, which are sets of subsets of X ∪ {z : z ∈ X}, and it weights subsets that contain x or x by their respective lengths: Definition 8 ([Hooker and Vinay, 1995]). Let D be a family of sets of literals. The two-sided Jeroslow-Wang value for a variable x is defined as We call a set C of literals trivial if there is a variable x such that x ∈ C and x ∈ C. For a variable x, say that D is x-orthogonal if for all C,C ′ ∈ D, C ̸= C ′ , there is a literal η ̸∈ {x, x} such that η ∈ C and η ∈ C ′ . Orthogonality is well-studied for DNFs [Crama and Hammer, 2011b]. The two-sided Jeroslow-Wang value and the influence agree up to a factor of two for some families of sets of literals when interpreting them as DNFs: Theorem 5. Let D be a family of sets of literals such that all of its elements are non-trivial, and let x be variable such that D is x-orthogonal. Then: A simple example that illustrates Theorem 5 would be D = {{x, y, z}, {y, z}}. Note that we can interpret D as a CNF as well, since the influence does not distinguish between a function and its dual (Theorem 1). Note that every Boolean function can be expressed by a family D that satisfies the conditions of Theorem 5. For this, we construct the canonical DNF corresponding to f and resolve all monomials that differ only in x. ## 4.3 Cooperative Game Mappings Attribution schemes analogous to what we call value functions were already studied in the context of game theory, most often with emphasis on Shapley- and Banzhaf values [Shapley, 1953; Banzhaf, 1965]. They are studied w.r.t. cooperative games, which are a popular way of modeling collaborative behavior. Instead of Boolean assignments, their domains are subsets (coalitions) of X. Specifically, cooperative games are of the form v : 2X → R, in which the value v(S) is associated with the payoff that variables (players) in S receive when collaborating. Since more cooperation generally means higher payoffs, they are often assumed to be monotonically increasing w.r.t. set inclusion. In its unconstrained form, they are essentially pseudo Boolean functions. We denote by G(X) the set of all cooperative games. If image(v) ⊆ {0, 1}, then we call v simple. For a cooperative game v, we denote by ∂xv the cooperative game that computes the "derivative" of v w.r.t. x, which is ∂xv(S) = v(S ∪{x})-v(S \{x}). We compose cooperative games using operations such as ·, +, -, ∧, ∨ etc., where (v ◦ w)(S) = v(S) ◦ w(S). For ∼ ∈ {≥,≤,=}, we also write v ∼ w if v(S) ∼ w(S) for all S ⊆ X. The set of variables v depends on is defined as dep(v) = {x ∈ X : ∂xv ̸= 0}. Cooperative game mappings map Boolean functions to cooperative games. Specific instances of such mappings have previously been investigated by [Hammer et al., 2000; Biswas and Sarkar, 2021]. We provide a general definition of this concept to show how it can be used to construct IVFs. Definition 9 (CGM). A cooperative game mapping (CGM) is a function τ : B(X) → G(X) with f ↦→ τf . We call τ importance inducing if for all x, y ∈ X, permutations σ : X → X, and f, g, h ∈ B(X): (MODECCG) ∂xτf ≥ ∂xτh if (i) f and h are monotonically modular in g, (ii) fg/1 ≥ hg/1 and hg/0 ≥ fg/0 and (iii) x ∈ dep(g). We call τ unbiased if τg = τg for all g ∈ B(X). An example is the characteristic CGM ζ given by ζf (S) = f(1S), where 1S(x) = 1 iff x ∈ S. We study various importance-inducing CGMs in the following sections. Note that ζ is not importance inducing: for example, it violates BOUNDCG since ∂xζf (∅) = -1 for f = x. The restriction to importance-inducing CGMs ensures that compositions with the Banzhaf or Shapley value are valid IVFs (Lemma 2). These CGMs satisfy properties that are related to Definition 2: τf should be monotone (0 ≤ ∂xτf ), irrelevant variables of f are also irrelevant for τf (DUMCG), etc. In an analogous fashion, we can think of properties related to Definition 3: ## Definition 10. A CGM τ is called - chain-rule decomposable, if for all f, g ∈ B(X) such that f is modular in g and x ∈ dep(g): where ∂gτf = ∂xg τf[g/xg] for some xg ̸∈ dep(f). We call τ weakly cain-rule decomposable if this holds for all cases where f is monotonically modular in g. - derivative dependent, if for all f, g ∈ B(X), x ∈ X Since (weak) rank-preservation for value functions uses an IVF in its premise, it cannot be stated naturally at the level of CGMs. Let us now define the following abstraction, which captures Shapley and Banzhaf values: Definition 11. Call E: X × G(X) → R, (x, v) ↦→ Ex(v) a value function for cooperative games. Call E an expectation of contributions if there are weights c(0), . . . , c(n-1) ∈ R such that for all v ∈ G(X) and x ∈ X: If E is an expectation of contributions, then Ex(v) is indeed the expected value of ∂xv(S) in which every S ⊆ X \ {x} has probability c(|S|). The Banzhaf and Shapley values are defined as the expectations of contributions with weights: Observe that there are (n-1 k ) sets of size k ∈ {0, . . . , n-1}, so the weights of the Shapley value indeed sum up to one. If τ is a CGM, then its composition with E yields (E ◦ τ)x(f) = Ex(τf), which is a value function for Boolean functions. Then every composition with an expectation of contributions is an IVF if the CGM is importance inducing: Lemma 2. If τ is an importance-inducing CGM and E an expectation of contributions, then E ◦ τ is an IVF. If τ is unbiased/derivative dependent, then so is E ◦ τ. Finally, if τ is (weakly) chain-rule decomposable, then so is Bz ◦ τ . In the following sections, we study two novel and the already-known CGM of [Hammer et al., 2000]. By Lemma 2 we can focus on their properties as CGMs, knowing that any composition with the Shapley value or other expectations of contributions will induce IVFs. ## Simple Satisfiability-Biased Cooperative Game Mappings The first CGM interprets the "power" of a coalition as its ability to force a function's outcome to one: If there is an assignment for a set of variables that yields outcome one no matter the values of other variables, we assign this set a value of one, and zero otherwise. Definition 12. The dominating CGM ω is defined as Example. Let f = x∨(y⊕z). We have ωf ({y, z}) = 1 since fu = 1 for u = y/1; z/0. On the other hand, ωf ({y}) = 0, since x/0; z/1 resp. x/0; z/0 falsify fy/1 and fy/0. Theorem 6. The dominating CGM is weakly chain-rule decomposable and importance inducing. Example. Let Z be the expectation of contributions with c(0) = 1, i.e., Zx(v) = v({x}) - v(∅). By Lemma 2 and Theorem 6, the mapping is an IVF. Intuitively, x has the highest importance if the function is falsifiable and there is a setting for x that forces the function to one. Otherwise, x has an importance of zero. Biasedness and rank preservation. The dominating CGM is biased: Consider g = x∨(y⊕z) with g = x∧(y⊕z). Note that ωg(S) = 1 for S = {x} while ωg(S) = 0, which shows biasedness. Composing ω with the Banzhaf value yields One can force g to one by controlling either x or both y and z, so x is rated higher than the others. But to force g to one, control over all variables is required, so all variables in g have the same importance. Since g is modular in g, we also obtain a counterexample for rank preservation: However, weak rank preservation is fulfilled by Bz ◦ ω since it is weakly chain-rule decomposable by Theorem 6 and Lemma 2. Then the claim follows with Theorem 1. A dual to the dominating CGM. One can think of a dual notion of the CGM ω that reverses the order of both quantifiers. Intuitively, we are now allowed to choose an assignment depending on the values of the remaining variables: Definition 13. The rectifying CGM ν is defined as If we compose ν with an expectation of contributions that satisfies c(k) = c(n-1-k) for all k ∈ {0, . . . , n-1}, which is a condition satisfied both by the Shapley and Banzhaf values, the induced importance of a variable equals its importance w.r.t. ω and the negated function: Proposition 3. Let E be an expectation of contributions with c(k) = c(n-1-k) for all k ∈ {0, . . . , n-1}. Then for all g ∈ B(X) and x ∈ X: We now discuss connections to the influence. If a Boolean function is monotone, and we "control" a set of variables S, the best towards satisfaction (resp. falsification) is to set all variables in S to one (resp. to zero). This can be used to show that both Bz ◦ ω and Bz ◦ ν agree with the influence: Proposition 4. Let f be a monotone Boolean function and x ## A Constancy-Based Cooperative Game Mapping Hammer, Kogan and Rothblum [Hammer et al., 2000] (HKR) defined a CGM that measures the power of variables by how constant they make a function if assigned random values. It depends on the following notion of constancy measure: Definition 14. We call a mapping κ: [0, 1] → [0, 1] a constancy measure if (i) κ is convex, (ii) κ(0) = 1, (iii) κ(x) = κ(1-x), and (iv) κ(1/2) = 0. The following functions are instances of constancy measures: - κquad(a) = 4(a- 1/2)2 , - κlog(a) = 1+alb(a)+(1-a)lb(1-a) with 0lb(0) = 0, - κabs(a) = 2|a- 1/2|. For a constancy measure κ and a Boolean function f, the κconstancy of f is the value κ(E[f ]), which measures how balanced the share of ones and zeros is. It is close to one if f is very unbalanced and close to zero if the share of zeros and ones in f is (almost) the same. The power of a set of variables S is now measured in terms of the expected κ-constancy of f if variables in S are fixed to random values: Definition 15 ([Hammer et al., 2000]). Given a constancy measure κ, we define the CGM Hκ by Example. Let f = x ∨ y ∨ z and S = {x}. We obtain Hκf (S) = 1/2 · κ(3/4) + 1/2 · κ(1), since Setting x to zero does not determine f completely, while setting it to one also sets f to one, i.e., makes it constant. The measure then gives a lower value to the less-constant cofactor, a higher value to the more-constant cofactor and computes the average. For this example and κ = κabs, we obtain Hκf (S) = 3/4 due to κ(3/4) = 1/2 and κ(1) = 1. Theorem 7 shows that Hκquad is a chain-rule decomposable and importance-inducing CGM. It is open whether other constancy measures are importance inducing too. Theorem 7. Suppose κ is a constancy measure. Then Hκ is an unbiased CGM that satisfies BOUNDCG, DICCG, DUMCG, and TYPECG. Further, Hκquad is chain-rule decomposable and satisfies MODECCG. Example. For the special case where κ = κquad, note that where Z is again the expectation of contributions with The value Z ◦ Hκ is an IVF according Lemma 2 and Theorem 7. In contrast to derivative-dependent IVFs, Z ◦ Hκ assigns low values to variables in parity-functions: for f = x⊕y, we have E[fx/1] = E[fx/0], and thus (Z◦Hκ )x(f ) = 0. Derivative dependence. This property cannot be achieved, as witnessed by f = x⊕y and g = x. Due to Dxf = Dxg, it suffices to show that ∂xHκf ̸= ∂xHκg holds for all κ. Note that and E[f] = E[g] = 1/2. Thus, for all constancy measures κ, which shows ∂xHκf ̸= ∂xHκg . ## 5 Computing Importance Values In this section, we present and evaluate computation schemes for blame, influence, and CGMs. While there exists a practical approach based on model counting for the influence in CNFs [Traxler, 2009], we are only aware of na¨ıve computations of CHK's blame [Dubslaff et al., 2022]. Blame. We focus on the modified blame. CHK's blame can be computed in a very similar fashion. Observe that for a Boolean function f and x ∈ X, where γk is the Boolean function for which γk(u) = 1 iff mscsux (f) ≤ k. We devise two approaches for computing E[γk]. The first represents γk through BDDs using the following recursion scheme: mscsux (f) ≤ k holds iff - k = 0 and f(u) ̸= f(flip{x}(u)), or - k > 0 and - mscsux (f) ≤ k-1 or - there is y ̸= x such that mscsux (f[y/y]) ≤ k-1. This allows us to construct BDDs for γk from γk-1, which lends itself to BDD-based approaches since γk does not necessarily increase in size as k grows. The second approach introduces new existentially quantified variables in the input formula of f to model occurrences of variables in critical sets of mscsux (f). With an additional cardinality constraint restricting the number of variables in critical sets to at most k, we can use projected model counting to compute E[γk]. Table 1: Computation time for instances of the ISCAS'99 dataset, timeout set to one hour. BDD columns Influence, DCGM (construction of the BDD for the dominating CGM), and Blame are without the BDD construction time for the initial CNF (cf. column Construction). | Instance | #Variables | #Clauses | (projected) model counting approaches - Influence (CNF) | (projected) model counting approaches - Influence (formula) | (projected) model counting approaches - Blame | BDD-based approaches - Construction | BDD-based approaches - Influence | BDD-based approaches - DCGM | Blame | |------------|--------------|------------|-----------------------------------------------------------|---------------------------------------------------------------|-------------------------------------------------|---------------------------------------|------------------------------------|-------------------------------|-------------| | b02 | 26 | 66 | 5 ms | 49ms | timeout | 1ms | <1ms | 2 ms | 3'649 ms | | b06 | 44 | 122 | 7 ms | 99ms | timeout | 3ms | <1ms | 6 ms | 697'573 ms | | b01 | 45 | 120 | 7 ms | 110ms | timeout | 4ms | <1ms | 8ms | 3'068'667ms | | b03 | 156 | 376 | 11 ms | 442ms | timeout | 53'934 ms | 24ms | 1'776ms | timeout | | b13 | 352 | 847 | 34 ms | 1'088ms | timeout | timeout | timeout | timeout | timeout | | b12 | 1'072 | 2'911 | 230 ms | 8'555ms | timeout | timeout | timeout | timeout | timeout | Figure 1: Computation of blame values on random (n, 3n, 7)-CNFs (number of variables, number of clauses, clause width). BDD times include construction time of the BDD for the initial CNF. ![Image](https://ijcai.org/proceedings/2023/fulltext/304/image_000000_0d961758ad823a4ef6971fb9f9b8b3d2693138ae4af5e7bbb70906a9da1e8895.png) Influence. In case f is given as a CNF formula, we use Traxler's method to compute the influence [Traxler, 2009]. For all other formulas, note that standard satisfiabilitypreserving transformations do not preserve influence values: For example, applying the Tseytin transformation to x∨xy results in a CNF where x has a higher influence than y. However, the influence is proportional to the number of models of Dxf. If f is given by a BDD, computing a representation of Dxf means squaring f's size in the worst case, while the formula-based representation only doubles it. For the latter case, we can count the models of Dxf using a Tseytin transformation and a standard model counter. BDD representations of satisfiability-biased CGMs. The dominating CGM computes a simple game, which is essentially a Boolean function, and therefore permits a representation by BDDs. Moreover, using a BDD representation of f, we compute ωf using a recursion on cofactors of variables z, The Banzhaf value of x in ωf is then just which poses no effort once the BDD of ωf is constructed. The rectifying CGM can be computed analogously. Implementation and evaluation. We have implemented Traxler's method and our new computation schemes in Python, using BuDDy [Lind-Nielsen, 1999] as BDD backend with automatic reordering and GPMC [Suzuki et al., 2015; Suzuki et al., 2017] for (projected) model counting. To evaluate our approaches, we conducted experiments on Boolean functions given as CNFs that were either randomly generated or generated from the ISCAS'99 dataset [Davidson, 1999; Compile! Project, 2023]. We always computed importance values w.r.t. the first variable in the input CNF and averaged the timings over 20 runs each. Our experiments were carried out on a Linux system with an i5-10400F CPU at 2.90GHz and 16GB of RAM. To compare our BDD-based and model counting approaches, Figure 1 shows timings for blame computations on random CNFs. Here, the BDD-based approach clearly outperforms the one based on projected model counting. This is also reflected in real-world benchmarks from ISCAS'99 shown in Table 1, where the approach based on model counting runs into timeouts for even small instances. Table 1 shows that computations for influence values based on model counting scale better than the BDD-based approach, mainly due to an expensive initial BDD construction. Computing the BDD of the dominating CGM is done without much overhead once the BDD for the CNF is given. ## 6 Conclusion This paper introduced IVFs as a way to formally reason about importance of variables in Boolean functions. We established general statements about IVFs, also providing insights on notions of importance from the literature by showing that they all belong to the class of IVFs. Apart from revealing several relations between known IVFs, we have shown how to generate new ones inspired by cooperative game theory. For future work, we will study properties with strict importance inequalities, IVFs for sets of variables, IVFs for pseudo Boolean functions, and global values similar to the total influence [O'Donnell, 2014]. On the empirical side, the generation of splitting rules for SAT-solvers and variable-order heuristics for BDDs based on different instances of IVFs are promising avenues to pursue. ## Acknowledgments The authors were partly supported by the DFG through the DFG grant 389792660 as part of TRR 248 and the Cluster of Excellence EXC 2050/1 (CeTI, project ID 390696704, as part of Germany's Excellence Strategy) and "SAIL: SustAInable Life-cycle of Intelligent Socio-Technical Systems" (Grant ID NW21-059D), funded by the program "Netzwerke 2021" of the Ministry of Culture and Science of the State of North Rhine-Westphalia, Germany. ## References 1. [Ashenhurst, 1957] Robert Ashenhurst. The Decomposition of Switching Functions. In Proceedings of an Interna- tional Symposium on the Theory of Switching, April 1957. 2. [Aziz et al., 2015] Rehan Abdul Aziz, Geoffrey Chu, Chris- tian Muise, and Peter Stuckey. #∃SAT: Projected model counting. In International Conference on Theory and Applications of Satisfiability Testing, pages 121-137. Springer, 2015. 3. [Banzhaf, 1965] John Francis Banzhaf. Weighted Voting Doesn't Work: A Mathematical Analysis. Rutgers Law Review, 19:317-343, 1965. 4. [Bartlett and Andrews, 2001] L. M. Bartlett and J. D. An- drews. Comparison of two new approaches to variable ordering for binary decision diagrams. Quality and Re- liability Engineering International, 17(3):151-158, May 2001. 5. [Ben-Or and Linial, 1985] Michael Ben-Or and Nathan Linial. Collective Coin Flipping, Robust Voting Schemes and Minima of Banzhaf Values. In 26th Annual Sympo- sium on Foundations of Computer Science (Sfcs 1985), pages 408-416, Portland, OR, USA, 1985. IEEE. 6. Jan C. Bioch. Decomposition of Boolean Functions. In Yves Crama and Peter L. Hammer, editors, Boolean Models and Methods in Mathematics, Computer Science, and Engineering, pages 39-76. Cambridge Uni- versity Press, first edition, June 2010. 7. [Birnbaum and Esary, 1965] Zygmunt Wilhelm Birnbaum Birnbaum and J. D. Esary. Modules of Coherent Binary Systems. Journal of the Society for Industrial and Applied Mathematics, 13(2):444-462, June 1965. 8. [Biswas and Sarkar, 2021] Aniruddha Biswas and Palash Sarkar. Influence of a set of variables on a boolean func- tion. Electron. Colloquium Comput. Complex., TR21-111, 2021. 9. [Bryant, 1992] Randal E. Bryant. Symbolic Boolean ma- nipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24(3):293-318, September 1992. 10. [Chockler and Halpern, 2004] Hana Chockler and Joseph Y. Halpern. Responsibility and Blame: A Structural-Model Approach. Journal of Artificial Intelligence Research, 22:93-115, October 2004. 11. [Chockler et al., 2008] Hana Chockler, Joseph Y. Halpern, and Orna Kupferman. What Causes a System to Satisfy a Specification? ACM Transactions on Computational Logic, 9(3):1-26, June 2008. 12. [Compile! Project, 2023] Compile! Project. Benchmarks. https://www.cril.univ-artois.fr/kc/benchmarks.html, 2023. Accessed: 2023-01-11. 13. [Crama and Hammer, 2011a] Yves Crama and Peter L. Hammer. Boolean Functions: Theory, Algorithms, and Applications. Encyclopedia of Mathematics and its Appli- cations. Cambridge University Press, 2011. 14. [Crama and Hammer, 2011b] Yves Crama and Peter L. Hammer. Orthogonal forms and shellability. In Boolean Functions: Theory, Algorithms, and Applications, Ency- clopedia of Mathematics and Its Applications, chapter 7, pages 326-350. Cambridge University Press, Cambridge, 2011. 15. [Davidson, 1999] Scott Davidson. Itc'99 benchmark circuits-preliminary results. In International Test Con- ference 1999. Proceedings (IEEE Cat. No. 99CH37034), pages 1125-1125. IEEE, 1999. 16. [Deng and Papadimitriou, 1994] Xiaotie Deng and Chris- tos H. Papadimitriou. On the complexity of cooperative solution concepts. Mathematics of Operations Research, 19(2):257-266, 1994. 17. [Dubslaff et al., 2022] Clemens Dubslaff, Kallistos Weis, Christel Baier, and Sven Apel. Causality in configurable software systems. In Proceedings of the 44th Interna- tional Conference on Software Engineering, ICSE '22, page 325-337, New York, NY, USA, 2022. Association for Computing Machinery. 18. [Faigle and Kern, 1992] Ulrich Faigle and Walter Kern. The shapley value for cooperative games under precedence constraints. International Journal of Game Theory, 21(3):249-266, 1992. 19. [Golomb, 1959] Solomon Golomb. On the classification of Boolean functions. IRE Transactions on Information The- ory, 5(5):176-186, May 1959. 20. [Hammer et al., 2000] Peter L. Hammer, Alexander Kogan, and Uriel G. Rothblum. Evaluation, Strength, and Rele- vance of Variables of Boolean Functions. SIAM Journal on Discrete Mathematics, 13(3):302-312, January 2000. 21. [Hooker and Vinay, 1995] John N. Hooker and V. Vinay. Branching rules for satisfiability. Journal of Automated Reasoning, 15(3):359-383, 1995. 22. [Jeroslow and Wang, 1990] Robert G. Jeroslow and Jin- chang Wang. Solving propositional satisfiability prob- lems. Annals of Mathematics and Artificial Intelligence, 1(1-4):167-187, September 1990. 23. [Kahn et al., 1988] Jeff Kahn, Gil Kalai, and Nathan Linial. The Influence of Variables on Boolean Functions. In [Pro- ceedings 1988] 29th Annual Symposium on Foundations of Computer Science, pages 68-80, October 1988. 24. [Lind-Nielsen, 1999] Jørn Lind-Nielsen. BuDDy: A binary decision diagram package. Department of Information Technology, Technical University of Denmark, 1999. 25. [Marques-Silva, 1999] João Marques-Silva. The Impact of Branching Heuristics in Propositional Satisfiability Algo- rithms. In G. Goos, J. Hartmanis, J. van Leeuwen, Pe- dro Barahona, and José J. Alferes, editors, Progress in Ar- tificial Intelligence, volume 1695, pages 62-74. Springer Berlin Heidelberg, Berlin, Heidelberg, 1999. 26. [O'Donnell, 2014] Ryan O'Donnell. Analysis of boolean functions. Cambridge University Press, 2014. 27. [Shapley, 1953] Loyd. S. Shapley. A Value for n-Person Games. In Harold William Kuhn and Albert William Tucker, editors, Contributions to the Theory of Games II, pages 307-318. Princeton University Press, December 1953. 28. [Shapley, 1967] Lloyd S. Shapley. Compound simple games, III: On committees. Technical report, RAND CORP SANTA MONICA CA, 1967. 29. [Slepian, 1953] David Slepian. On The Number of Symme- try Types of Boolean Functions of n Variables. Canadian Journal of Mathematics, 5:185-193, 1953. 30. [Suzuki et al., 2015] Ryosuke Suzuki, Kenji Hashimoto, and Masahiko Sakai. An Extension of a DPLL-Based Model- Counting Solver for Projected Model. JSAI Technical Re- port, SIG-FPAI-97-B404:59-64, March 2015. 31. [Suzuki et al., 2017] Ryosuke Suzuki, Kenji Hashimoto, and Masahiko Sakai. Improvement of Projected Model- Counting Solver with Component Decomposition Using SAT Solving in Components. JSAI Technical Report, SIG- FPAI-103-B506:31-36, March 2017. 32. [Traxler, 2009] Patrick Traxler. Variable influences in con- junctive normal forms. In International Conference on Theory and Applications of Satisfiability Testing, pages 101-113. Springer, 2009.