reptheorem[1]

###### Theorem 0.1

# From Checking to Inference: Actual Causality Computations as Optimization
Problems††thanks: Extended version with proofs of ATVA2020 paper with the same
title. Work supported by the German Research Foundation (DFG) under grant no.
PR1266/4-1, Conflict resolution and causal inference with integrated socio-
technical models.

Amjad Ibrahim Department of Informatics, Technical University of Munich,
Germany Alexander Pretschner
Department of Informatics, Technical University of Munich, Germany {ibrahim,
<EMAIL_ADDRESS>
###### Abstract

Actual causality is increasingly well understood. Recent formal approaches,
proposed by Halpern and Pearl, have made this concept mature enough to be
amenable to automated reasoning. Actual causality is especially vital for
building accountable, explainable systems. Among other reasons, causality
reasoning is computationally hard due to the requirements of counterfactuality
and the minimality of causes. Previous approaches presented either inefficient
or restricted, and domain-specific, solutions to the problem of automating
causality reasoning. In this paper, we present a novel approach to formulate
different notions of causal reasoning, over binary acyclic models, as
optimization problems, based on quantifiable notions within counterfactual
computations. We contribute and compare two compact, non-trivial, and sound
integer linear programming (ILP) and Maximum Satisfiability (MaxSAT) encodings
to check causality. Given a candidate cause, both approaches identify what a
minimal cause is. Also, we present an ILP encoding to infer causality without
requiring a candidate cause. We show that both notions are efficiently
automated. Using models with more than $8000$ variables, checking is computed
in a matter of seconds, with MaxSAT outperforming ILP in many cases. In
contrast, inference is computed in a matter of minutes.

##  1 Introduction

Actual causality is the retrospective linking of effects to causes [13, 30].
As part of their cognition, humans reason about actual causality to explain
particular past events, to control future events, or to attribute moral
responsibility and legal liability [14]. Similar to humans, it is useful for
systems in investigating security protocols [21], safety accidents [22],
software or hardware models [5, 23, 9], and database queries [28]. More
importantly, actual causality is central for enabling social constructs such
as accountability in Cyber-Physical systems [16, 19, 17], in information
systems [10], and explainability in artificial intelligence systems [29].

Attempts to formalize a precise definition of an actual cause go back to the
eighteenth century when Hume [15] introduced counterfactual reasoning. Simply
put, counterfactual reasoning concludes that event $A$ is a cause of event $B$
if $B$ does not occur if $A$ does not occur. However, this simple reasoning
cannot be used with interdependent, multi-factorial, and complex causes [24].
Recently, Halpern and Pearl formalized HP–a seminal model-based definition of
actual causality that addresses many of the challenges facing naive
counterfactual reasoning [13].

Because of its formal foundation, HP enables automated causality reasoning. We
distinguish two notions of reasoning: checking and inference. Checking refers
to verifying if a candidate cause is an actual cause of an effect, i.e.,
answering the question “is $\vec{X}$ a cause of $\varphi$?” Inference involves
finding a cause without any candidates, i.e., answering the question “why
$\varphi$?” Using HP, causality checking is, in general, $D^{P}_{1}$-complete
and $\mathit{NP}$-complete for singleton (one-event) causes [12]; the
difference is due to a minimality requirement in the definition (details in
Section 2). Intuitively, inference is at least as hard. The complexity led to
restricted (e.g., singleton causes, single-equation models [28]) utilizations
of HP (Section 5). All these utilizations exploit domain-specificities (e.g.,
database repairs [28, 33] [6]), which hinders taking advantage of the
available approximations for general queries. In prior work, we proposed an
approach to check causality in acyclic models with binary variables based on
the satisfiability problem (SAT) [18]. The approach required enumerating all
the satisfying assignments of a formula (ALL-SAT), which obviously is impacted
by the solver’s performance [35]. Thus, previous approaches fail to automate
answering queries for larger models.

Large models of causal factors are likely to occur especially when generated
automatically from other sources for purposes of accountability and
explainability [17, 16, 29]. Further, models of real-world accidents are
sufficiently large to require efficient approaches. For instance, a model of
the 2002 mid-air collision in Germany consists of 95 factor [34] (discussed in
[17]). Thus, in this paper, we present a novel approach to formulate actual
causality computations in binary models as optimization problems. We show how
to construct quantifiable notions within counterfactual computations, and use
them for checking and inference.

We encode our checking approach as integer linear programs (ILP), or weighted
MaxSAT formulae [25]. Both are well-suited alternatives for Boolean
optimization problems. However, MaxSAT has an inherent advantage with binary
propositional constraints [25]. On the other hand, ILP has an expressive
objective language that allows us to tackle the problem of causality inference
as a multi-objective program. Accordingly, we contribute an approach with
three encodings. The first two cover causality checking, and better they can
determine a minimal HP cause from a potentially non-minimal candidate cause;
we refer to this ability as semi-inference. The third encoding tackles
causality inference. All these encodings benefit from the rapid development in
solving complex and large (tens of thousands of variables and constraints)
optimization problems [20, 2].

We consider our work to be the first to provide an efficient solution to the
problem of checking and inferring HP causality, for a large class of models
(binary models) without any dependency on domain-specific technologies. We
contribute: 1.) A sound formulation of causality computations for acyclic
binary models as optimization problems, 2.) A Java
library111https://github.com/amjadKhalifah/HP2SAT1.0/tree/hp-optimization-
library that implements the approaches. 3.) An empirical evaluation, using
models from multiple domains, of the efficiency and scalability of the
approaches in comparison with previous work.

##  2 Halpern-Pearl Definition of Actual Causality

HP uses variables to describe the world, and structural equations to define
its mechanics [30]. The variables are split into exogenous and endogenous. The
values of the former, called a context $\vec{u}$, are governed by factors that
are not part of the modeled world (they represent the environment). The
endogenous variables, in contrast, are determined by equations of exogenous
and endogenous variables. In this formulation, we look at causes within a
specified universe of discourse represented by the endogenous variables, while
exogenous variables are not considered to be part of a cause but rather as
given information. An equation represents the semantics of the dependency of
the endogenous variable on other variables. Similar to Halpern, we limit
ourselves to acyclic models in which we can compute a unique solution for the
equations given a context $\vec{u}$, which we refer to as actual evaluation of
the model. A binary model (Boolean variables only) is formalized in 1.

###### Definition 1

[30] Binary Causal Model
A causal model is a tuple $M=\mathcal{(U,V,R,F)}$, where
\- $\mathcal{U}$, $\mathcal{V}$ are sets of exogenous variables and endogenous
variables respectively,
\- $\mathcal{R}$ associates with $Y\in\mathcal{U\cup V}$ a set of possible
values $\mathcal{R}(Y)$, i.e., $\\{0,1\\}$,
\- $\mathcal{F}$ maps $X\in\mathcal{V}$ to a function
$F_{X}\mathrel{\mathop{\mathchar
58\relax}}(\times_{U\in\mathcal{U}}\mathcal{R}(U))\times(\times_{Y\in\mathcal{V}\backslash\\{X\\}}\mathcal{R}(Y))\to\\{0,1\\}$

1 makes precise the fact that $F_{X}$ determines the value of $X$, given the
values of all the other variables. We summarize the causality notations before
defining the cause in 2. A primitive event is a formula of the form $X=x$, for
$X\in\mathcal{V}$ and $x$ is a value $\in\\{0,1\\}$. A sequence of variables
$X_{1},...,X_{n}$ is abbreviated as $\vec{X}$. Analogously,
$X_{1}=x_{1},...,X_{n}=x_{n}$ is abbreviated $\vec{X}=\vec{x}$. $\varphi$ is a
Boolean combination of such events. $(M,\vec{u})\models X=x$ if the variable
$X$ has value $x$ in the unique solution to the equations in $M$ given context
$\vec{u}$. The value of variable $Y$ can be overwritten by a value $y$ (known
as an intervention) writing $Y\leftarrow y$ (analogously
$\vec{Y}\leftarrow\vec{y}$ for vectors). Then, a causal formula is of the form
$[Y_{1}\leftarrow y_{1},...,Y_{k}\leftarrow y_{k}]\varphi$, where
$Y_{1},...,Y_{k}$ are variables in $\mathcal{V}$ that make $\varphi$ hold when
they are set to $y_{1},..,y_{k}$. We write $(M,\vec{u})\models\varphi$ if the
causal formula $\varphi$ is true in $M$ given $\vec{u}$. Lastly,
$(M,\vec{u})\models[\vec{Y}\leftarrow\vec{y}]\varphi$ holds if we replace
variable equations’ in $\vec{Y}$ by equations of the form $Y=y$ denoted by
$(M_{\vec{Y}=\vec{y}},\vec{u})\models\varphi$ [13].

###### Definition 2

Actual Cause [12]
$\vec{X}=\vec{x}$ is an actual cause of $\varphi$ in $(M,\vec{u})$ if the
following three conditions hold:
AC1. $(M,\vec{u})\models(\vec{X}=\vec{x})$ and $(M,\vec{u})\models\varphi$.
AC2. There is a set $\vec{W}$ of variables in $\mathcal{V}$ and a setting
$\vec{x}^{\prime}$ of the variables in $\vec{X}$ such that if
$(M,\vec{u})\models\vec{W}=\vec{w}$, then
$(M,\vec{u})\models[\vec{X}\leftarrow\vec{x}^{\prime},\vec{W}\leftarrow\vec{w}]\neg\varphi$.
AC3. $\overrightarrow{X}$ is minimal: no non-empty subset of $\vec{X}$
satisfies AC1 and AC2.

AC1 checks that the cause $\vec{X}=\vec{x}$ and the effect $\varphi$ occurred
within the actual evaluation of $M$ given context $\vec{u}$, i.e., the cause
is sufficient for the occurrence of the effect. AC2 checks the counterfactual
(necessary) relation between the cause and effect. It holds if there exists a
setting $\vec{x}^{\prime}$ for the cause variables $\vec{X}$ different from
the actual evaluation $\vec{x}$ (in binary models such a setting is the
negation of the actual setting [18]), and another set of variables $\vec{W}$,
referred to as a contingency set, that we use to fix variables at their actual
values, such that $\varphi$ does not occur. The contingency set $\vec{W}$ is
meant to deal with issues such as preemption and redundancy. Preemption is a
problematic situation where multiple possible causes coincide (illustrated by
an example below) [24]; thus a naive counterfactual check cannot determine the
cause [23]. AC3 checks that $\vec{X}$ is minimal in fulfilling the previous
conditions. To check a cause, we need to think of two worlds (variable
assignments): the actual world with all the values known to us, and the
counterfactual one in which the cause and effect take on different values. Two
factors further complicate the search for this counterfactual world. First,
finding an arbitrary $\vec{W}$, such that AC2 holds which is exponential in
the worst case. Second, no (non-empty) subset of $\vec{X}$ is sufficient for
constructing such a counterfactual world. Halpern shows that checking
causality is in general $D^{P}_{1}$-complete [12, 1], i.e., checking AC1 is
$P$, checking AC2 is $NP$-complete, and checking AC3 is $co-NP$-complete.
Complexity considerations for binary models suggest a reduction to SAT or ILP
[12]; in this paper, we show concrete ILP and MaxSAT formulations to check,
and an ILP formulation to infer a cause.

Example: Throwing rocks [24] is a problematic example from philosophy: Suzy
and Billy both throw a rock at a bottle that shatters if one of them hits. We
know Suzy’s rock hits the bottle slightly earlier than Billy’s and both are
accurate throwers. Halpern models this story using the endogenous variables
$ST,$ $BT$ for “Suzy/Billy throws”, with values 0 (the person does not throw)
and 1 (s/he does), $SH,BH$ for “Suzy/Billy hits”, and $BS$ for “bottle
shatters.” Two exogenous variables $ST_{exo},BT_{exo}$ are used to set the
values. The equations:

– $ST=ST_{exo}$– $BT=BT_{exo}$ – $SH=ST$
– $BH=BT\land\neg SH$ – $BS=SH\lor BH$

Assuming a context (exogenous variables’ values) $\vec{U}=\vec{u}$:
$ST_{exo}=1,BT_{exo}=1$ (both actually threw), the actual evaluation of the
model is: $ST=1$, $BT=1$, $BH=0$, $SH=1$, and $BS=1$. Assume we want to check
whether $ST=1$ is a cause of $BS=1$, i.e., is Suzy’s throw a cause for the
bottle shattering? Obviously, AC1 is fulfilled as both appear in the actual
evaluation. As a candidate cause, we set $ST=0$ (for binary models a candidate
cause is negated to check counterfactuality; see Lemma 1 in [18]). A first
attempt with $\vec{W}=\emptyset$ shows that AC2 does not hold. However, if we
randomly let $\vec{W}=\\{BH\\}$, i.e., we replace the equation of $BH$ with
$BH=0$, then AC2 holds because $(M,\vec{u})\models[ST\leftarrow 0,BH\leftarrow
0]BS=0$, and AC3 automatically holds since the cause is a singleton. Thus,
$ST=1$ is a cause of $BS=1$. Let us check if $ST=1\land BT=1$ is a cause for
$BS=1$. AC1 and AC2 hold (obviously if they both did not throw, the bottle
would not shatter with a $\vec{W}=\emptyset$) but AC3 does not. As we saw
earlier, $ST=1$ alone satisfies AC2. Hence $ST=1\land BT=1$ are not a cause.

As opposed to the all-or-nothing treatment of causality, Chockler and Halpern
added ([8], modified in [13]) a notion of responsibility to a cause. They
introduced a metric, degree of responsibility ($dr$), that “measures the
minimal number of changes needed to make $\varphi$ counterfactually depend on
$X$.”222Their idea is often motivated with an example of $11$ voters that can
vote for Suzy or Billy. If Suzy wins $6$-$5$, we can show that each Suzy voter
is a cause of her winning. If Suzy wins $11$-$0$, then each subset of size six
of the voters is a cause. The authors argue that in $11$-$0$ scenario, “a
voter feels less responsible” compared to $6$-$5$ situation. 3 shows a
shortened version of $dr$ [8, 13], which we use for causality inference in our
work.

###### Definition 3

The degree of responsibility of $X=x$ w.r.t. a cause $\vec{X}=\vec{x}$ for
$\varphi$, denoted $dr((\vec{X}=\vec{x}),(X=x),\varphi)$, is $0$ if $X=x$ is
not in $\vec{X}=\vec{x}$; otherwise is $1/(|\vec{W}|+|\vec{X}|)$ given that
$|\vec{W}|$ is the smallest set of variables that satisfies AC2.

##  3 Approach

Given the triviality of AC1, we presented in prior work, a SAT-based approach
to check causality, focusing on AC2 [18]. The contribution was in how AC2 is
encoded into a formula $F$, so that an efficient conclusion of $\vec{W}$
without iterating over the power-set of all variables, is possible. Briefly,
$F$ described a counterfactual world that incorporated (1) $\neg\varphi$, (2)
a context $\vec{u}$ (size $n$), (3) a setting $\vec{x}^{\prime}$ for a
candidate cause, $\vec{X}$, and (4) a method to infer $\vec{W}$, while
maintaining the semantics of $M$. Because checking is done in hindsight, we
have the actual evaluation of the variables. Thus, the first three
requirements are represented using literals. The semantics of $M$, given by
each function $F_{V_{i}}$ corresponding to $V_{i}$ (according to 1), is
expressed using an equivalence operator between a variable and its function,
i.e., $V_{i}\leftrightarrow F_{V_{i}}$. This is not done for the cause
variables because they are represented by a negation. To account for
$\vec{W}$, we add a disjunction to the equivalence sub-formula with the
positive or negative literal of $V_{i}$, according to its actual evaluation
($1$ or $0$). With this representation of each variable, we check if such a
counterfactual world is satisfiable, and hence AC2 holds.

By generalizing $F$, we can also check minimality (AC3). Assume we remove the
restriction on the cause variables $\vec{X}$, of only be negated literals
(allowing them to take on their original values also), and call the new
formula $G$. Then $G$ might be satisfiable for the negated cause
$\vec{X}=\vec{x^{\prime}}$ as well as all the other combinations of the cause
set. Analyzing all the satisfying assignments of $G$ (All-SAT), allows us to
check minimality. Specifically, if we find an assignment such that at least
one conjunct of $\vec{X}=\vec{x}$ takes on a value that equals the one
computed from its equation, it means that it is not a required part of the
cause, and hence, the cause is not minimal. In many situations, All-SAT is
problematic and decreases the performance, especially if $G$ is satisfiable
for a large number of assignments [35]. Equation 1 shows the construction of
$G$. Because $Y_{i}$ is the variable form, and $y_{i}$ is the value, we use
$f(Y_{i}=y_{i})$ to convert the variable to a positive or a negative literal,
i.e., $Y$ or $\neg Y$.

$\displaystyle G\mathrel{\mathop{\mathchar
58\relax}}=\neg\varphi\wedge\bigwedge\limits_{i=1\ldots
n}f(U_{i}=u_{i})\wedge\bigwedge\limits_{i=1\ldots m,\not\exists j\bullet
X_{j}=V_{i}}\left(V_{i}\leftrightarrow F_{V_{i}}\lor f(V_{i}=v_{i})\right)$
(1)

$F$ and $G$ aid us in checking if a candidate cause $\vec{X}$ is a minimal,
counterfactual cause of $\varphi$. If it is not, we cannot use them to find a
minimal cause from within $\vec{X}$, i.e., semi-inference. We, also, cannot
use them to find a cause without requiring a candidate cause, i.e., inference.
To efficiently achieve such abilities, we present a novel formulation of
causal queries as optimization problems.

###  3.1 Checking and Semi-inference Queries as Optimization Problems

In this section, we focus on the computation of the minimality requirement in
causality checking. For that, we conceptualize a technique to check AC2 and
AC3 as one problem (AC1 is explicitly checked solely). The result of solving
this problem can then be interpreted to conclude AC2, $\vec{W}$, AC3, and,
better, what is a minimal subset of the cause if AC3 is violated (semi-
inference). To compare the efficiency, we formulate the problem as an integer
program, and a MaxSAT formula. Both techniques solve the problem based on an
objective function— a function whose value is minimized or maximized among
feasible alternatives.

To quantify an objective for a causal check, we introduce an integer variable
that we call the distance. Similar to the Hamming distance, it measures the
difference between the cause values when $\varphi$ holds true, i.e., actual
world, and when it holds false, i.e., the counterfactual world. As shown in
Equation 2, it is computed by counting the cause variables whose values
assigned by a solver ($x_{i}^{\prime}$) is different from their value under
the given context ($x_{i}$). As we shall see, the distance is equivalent to
the size of the (minimal) cause within our check of a possibly non-minimal
cause. As such, the distance must be greater than $0$, since a cause is non-
empty, and less or equal to the size of $\vec{X}$ ($\ell$), i.e., $1\leq
distance\leq\ell$.

$distance=\sum_{i=1}^{\ell}d(i)\qquad s.t\qquad
d(i)=\begin{cases}1-x_{i}^{\prime},&x_{i}=1\\\
x_{i}^{\prime},&x_{i}=0\end{cases}$ (2)

According to AC3, our objective function is then to minimize the distance; we
encode a causality check as an optimization problem that minimizes the number
of cause variables while satisfying the constraints for AC2 (counterfactuality
and $\vec{W}$). In the following, we present how to derive these constraints
for the ILP formulation, and the MaxSAT encoding. Then, we discuss how to
interpret the results to (semi-)infer a minimal cause from a possibly non-
minimal cause.

ILP is an optimization program with integer variables and linear constraints
and objectives. To formulate such a program, we need three elements: decision
variables, constraints, and objective(s). Our decision variables are, in
addition to the distance, the set of exogenous and endogenous variables from
the model, i.e., $\vec{U}\cup\vec{V}$. Since we only consider binary
variables, their values are bound to be $0$ or $1$. Since ILP and SAT solvers
can be used as complementary tools, the translation from SAT to ILP is
standard [26]. Therefore, we reuse formula $G$ (Equation 1) to create the
constraints. Constraints from $G$ contain the a.) effect not holding true, b.)
the context, c.) each endogenous variable either follows the model equation or
the actual value, i.e., part of the set $\vec{W}$, d.) each element in the
cause set $\vec{X}=\vec{x}$ is not constrained, i.e., its equation is removed.
Transforming these constraints (on the Conjunctive Normal Form (CNF) level)
into linear inequalities is straightforward; we have clauses that can be
reduced to ILP directly, e.g., express $y=x_{1}\lor x_{2}$ as $1\geq
2*y-x_{1}-x_{2}\geq 0$ [26]. In addition, we add a constraint to calculate the
distance according to Equation 2.

MaxSAT. The maximum satisfiability problem (MaxSAT) is an optimization variant
of SAT [25]. In contrast to SAT, which aims to find a satisfying assignment of
all the clauses in a formula, MaxSAT aims to find an assignment that maximizes
the number of satisfied clauses. Thus, MaxSAT allows the potential that some
clauses are unsatisfied. In this paper, we use partial MaxSAT solving, which
allows specific clauses to be unsatisfied, referred to as soft clauses;
contrary to the hard clauses that must be satisfied [25]. A soft clause can be
assigned a weight to represent the cost of not satisfying it. In essence, a
weighted partial MaxSAT problem is a minimization problem that minimizes the
cost over all solutions. Unlike ILP, the objective in MaxSAT is immutable.
Thus, we need to construct our formula in a way that mimics the concept of the
distance.

As shown in Equation 3, the MaxSAT encoding also uses $G$ (shown in Equation
1) as a base. $G$ embeds all the mandatory parts of any solution. Thus, we use
the CNF clauses of $G$ as hard clauses. On the other hand, we need to append
the cause variables ($\vec{X}$) as soft clauses (underlined in Equation 3).
Since the solver would minimize the cost of unsatisfying the ($\vec{X}$)
clauses, we represent each cause variable as a literal according to its
original value (when $\varphi$ holds). Because this is already in CNF, it is
easier to assign weights. We assign $1$ as a cost for unsatisfying each cause
variable’s clause, i.e., when $X_{i}$ is negated in the (solved)
counterfactual world. Then, the overall cost of unsatisfying the underlined
parts of the formula is the count of the negated causes, i.e., the size of the
minimal cause. Essentially, this concept maps directly to the distance, which
the MaxSAT solver will minimize. In contrast to ILP, we cannot specify a lower
bound on the MaxSAT objective. Thus, we need to express the non-emptiness of a
cause, as hard clauses. A non-empty cause means that at least one cause
variable $X_{j}$ does not take its original value, and does not follow its
equation due to an intervention. The first conjunction (after $G$) in Equation
3 ensures the first requirement, while the second corresponds to the second
case.

$\displaystyle G_{max}\mathrel{\mathop{\mathchar
58\relax}}=G\wedge\neg(\bigwedge\limits_{i=1\ldots\ell}f(X_{i}=x_{i}))\land\neg(\bigwedge\limits_{i=1\ldots\ell}X_{i}\leftrightarrow
F_{X_{i}})\underline{\wedge\bigwedge\limits_{i=1\ldots\ell}f(X_{i}=x_{i})}$
(3)

Results. With the above, we illustrated the formulation of a causal checking
problem. We now discuss how to translate their results to a causal answer once
they are solved; Algorithm 1 formalizes this. The evaluation, in the input, is
a list of the variables in $M$ and their values under $\vec{u}$. Assuming
$\vec{C}$ is a representation of the optimization problem (a set of linear
constraints (without the objective), or hard/soft clauses), then in Line 3, we
solve this problem and process the results in Lines 4-5. The feasibility
(satisfiability) of the problem implies that either $\vec{X}$ or a non-empty
subset of it is a minimal cause (fulfills AC2 and AC3). If distance (cost
returned by the MaxSAT solver) equals the size of $\vec{X}$, then the whole
candidate cause is minimal. Otherwise, to find a minimal cause $\vec{X}_{min}$
(semi-inference), we choose the parts of $\vec{X}$ that have different values
between the actual and the solved values (Line 4). To determine $\vec{W}$, in
Line 5, we take the variables whose solved values are the same as the actual
evaluation (potentially including $\vec{X}$ variables). Obviously, this is not
a minimal $\vec{W}$, which is not a requirement for checking HP [18]. If the
model is infeasible or unsatisfiable, then HP for the given $\vec{X}$
(checking) and its subsets (semi-inference) does not hold.

Algorithm 1 Interpreting the Optimization Problem’s Results

1:causal model $M$, context $\langle U_{1},\ldots,U_{n}\rangle=\langle
u_{1},\ldots,u_{n}\rangle$, effect $\varphi$, candidate cause $\langle
X_{1},\ldots,X_{\ell}\rangle=\langle x_{1},\ldots,x_{\ell}\rangle$, evaluation
$\langle V_{1},\ldots,V_{m}\rangle=\langle v_{1},\ldots,v_{m}\rangle$

2:function
CheckCause($M,\vec{U}=\vec{u},\varphi,\vec{X}=\vec{x},\vec{V}=\vec{v}$)

3: if $\langle U_{1}=u_{1}\ldots U_{n}=u_{n},V_{1}=v_{1}^{\prime}\ldots
V_{m}=v_{m}^{\prime}\rangle=$ $\textit{solve}(\vec{C},\textit{objective})$
then

4: $\vec{X}_{min}\mathrel{\mathop{\mathchar 58\relax}}=\langle
X^{\prime}_{1}...X^{\prime}_{d}\rangle$ s.t. $\forall i\forall
j\bullet(i\not=j\Rightarrow$
$X^{\prime}_{i}\not=X^{\prime}_{j})\wedge(X^{\prime}_{i}=V_{j}\Leftrightarrow
v_{j}^{\prime}\not=v_{j})$

5: $\vec{W}\mathrel{\mathop{\mathchar 58\relax}}=\langle W_{1}...W_{s}\rangle$
s.t. $\forall i\forall j\bullet(i\not=j\Rightarrow$
$W_{i}\not=W_{j})\wedge(W_{i}=V_{j}\Leftrightarrow v_{j}^{\prime}=v_{j})$

6: return $\vec{X}_{min},\vec{W}$

7: else return infeasible (unsatisfiable)

8: end if

9:end function

Throwing rocks Example: To illustrate our approach, we show the ILP and MaxSAT
encodings to answer the query is $ST=1,BT=1$ a cause of $BS=1$?

$\displaystyle min\enspace d\enspace\textrm{s.t.}$
$\displaystyle\\{BS=0,\enspace ST_{exo}=1,\enspace BT_{exo}=1,\enspace-
SH+BS\geq 0,\enspace-BH+BS\geq 0,$ $\displaystyle-ST+SH\geq 0,\enspace BT-
BH\geq 0,\enspace-SH-BH\geq-1,\enspace ST+BT+d=2\\}$ $\displaystyle
G_{max}\enspace\enspace=$ $\displaystyle\neg BS\;\land\;ST_{exo}\land
BT_{exo}\;\land\;(BS\leftrightarrow SH\lor BH)\;\land\;((SH\leftrightarrow
ST)\lor SH)\;\land$ $\displaystyle((BH\leftrightarrow BT\land\neg SH)\lor\neg
BH)\;\land\;\neg(ST\land BT)\;\land\;\underline{(ST\land BT)}$

Both encodings are solved with a $distance(d)$ (cost) value of $1$, which
indicates that $ST,BT$ is not minimal, and a cause of size $1$ is
(semi)-inferred, namely $ST$. The optimal assignment ($\neg
BS,ST_{exo},BT_{exo},\neg SH,\neg BH,\neg ST,BT$) showed that the constraints
can be guaranteed without changing the value of $BT$, which violates AC3. This
shows the enhancement of finding a minimal cause rather than only checking
AC3. Subsection 3.1 states the soundness of our approach (for proofs see
Appendix 0.A) ilp The generated optimization problem (ILP program or
$G_{max}$) is feasible iff AC3 holds for $\vec{X}$ or a non-empty subset of
$\vec{X}$.

###  3.2 Causality Inference with ILP

The previous approaches utilized the candidate cause $\vec{X}$ to help
describe a counterfactual world that proves $\vec{X}$ is a cause of $\varphi$.
In this section, we present a method, $ILP_{why}$, to infer causality (answer
why $\varphi$? questions) without requiring $\vec{X}$. Unlike checking, in
inference, we cannot aid the solver in a description of the counterfactual
world (e.g., negating values of $\vec{X}$). Instead, we describe
characteristics of the actual cause that have caused an effect $\varphi$.

In addition to requirements of counterfactuality and minimality imposed by the
conditions in 2, we utilize the degree of responsibility ($dr$) as a mean to
compare actual causes [8]. While the conditions are suitable for determining
if $\vec{X}$ is a cause, $dr$ judges the “quality” of the cause based on an
aggregation of its characteristics. Because we may find multiple causes for
which the conditions hold, $dr$ is reasonable for comparison. We require our
answer to an inference question to be an actual cause with the maximum $dr$.
We come back to this after we construct a formula $G^{*}$ that is the base of
$ILP_{why}$.

Both negating the effect formula ($\neg\varphi$) and setting the context
$f(U_{i}=u_{i})$ remain as in Equation 1. Because the variables that appear in
the effect formula cannot be part of the cause, we represent each with the
simple equivalence relation, i.e., $V_{i}\leftrightarrow F_{V_{i}}$. The
complicated part is representing the other variables because any variable can
be: a. a cause, b. a contingency-set, or c. a normal variable. Recall, in a
counterfactual computation, a cause does not follow its equation, and differs
from its original value; a contingency-set variable does not follow its
equation while keeping its original value; a normal variable follows its
equation, regardless of whether it equals the original value or not. Thus, we
need to allow variables to be classified in any category in the “best”
possible way.

To that end, we represent each (non-effect) variable $V_{i}$ with a
disjunction between the equivalence holding and not holding, and a disjunction
between its original value and its negation: $\left(\left(V_{i}\leftrightarrow
F_{V_{i}}\right)\lor\neg\left(V_{i}\leftrightarrow
F_{V_{i}}\right)\right)\wedge\left(V_{i_{orig}}\lor\neg V_{i_{orig}}\right)$.
Clearly, each disjunction is a tautology. However, this redundancy facilitates
the classification into the categories; more importantly, we can incentivize
the solver to classify those variables according to specific criteria.

To be able to guide the solver, we add auxiliary boolean variables
(indicators) to each clause (left and right parts of a disjunction). They
serve two functions. The first is to indicate which clauses hold. Since the
two parts of the conjunction are not mutually exclusive, i.e., a variable can
follow its equation, yet have its original value, we need two indicators
$C^{1}C^{2}$. Secondly, similar to the concept of distance from Subsection
3.1, we use the indicators to describe criteria of the solution. For each
variable $V_{i}$, $C^{1}_{i}$ is appended to the first two clauses:
$\left(\left(V_{i}\leftrightarrow F_{V_{i}}\right)\land
C^{1}_{i}\right)\lor\left(\neg\left(V_{i}\leftrightarrow
F_{V_{i}}\right)\land\neg C^{1}_{i}\right)$. Similarly $C^{2}$ is appended to
the other clauses. As such, the category of each endogenous variable is
determined based on values of $C^{1}$ and $C^{2}$. A cause variable would have
a $C^{1}C^{2}\mathrel{\mathop{\mathchar 58\relax}}00$ (not following the
formula nor its original value); a contingency-set variable has a
$C^{1}C^{2}\mathrel{\mathop{\mathchar 58\relax}}01$; and a normal variable has
a $C^{1}C^{2}\mathrel{\mathop{\mathchar 58\relax}}10$, or $11$. Formula
$G^{*}$ follows (equivalence relations of effect variables are omitted for
space).

$\displaystyle G^{*}\mathrel{\mathop{\mathchar 58\relax}}=$
$\displaystyle\neg\varphi\wedge\bigwedge_{i=1\ldots
n}f(U_{i}=u_{i})\wedge\bigwedge_{i=1\ldots
m}\left(\left(\left(V_{i}\leftrightarrow F_{V_{i}}\right)\land
C^{1}_{i}\right)\lor\left(\neg\left(V_{i}\leftrightarrow
F_{V_{i}}\right)\land\neg C^{1}_{i}\right)\right)$
$\displaystyle\land\left(\left(V_{orig}\land C^{2}_{i}\right)\lor\left(\neg
V_{orig}\land\neg C^{2}_{i}\right)\right)$

why Formula $G^{*}$ is satisfiable iff $\exists$ $\vec{X}=\vec{x}$ such that
AC2 holds for $\vec{X}$

We now discuss the objectives of this formulation. We aim to find an
assignment to the constraints in $G^{*}$ that corresponds to a cause with a
maximum $dr$. Recall that $dr$ is $1/(|\vec{X}|+|\vec{W}|)$. Maximizing $dr$
entails minimizing $|X|+|W|$. Since the three sets (cause, contingency, and
normal) form the overall model size (excluding effect and exogenous
variables), then minimizing $|X|+|W|$ is equivalent to maximizing the number
of normal variables, which concludes our first objective. The sum of $C^{1}$
variables resembles the number of normal variables; thus, $objective_{1}$ is
to maximize the sum of $C^{1}$ variables.

The above formulation minimizes $\vec{X}$, and $\vec{W}$ as a whole, following
$dr$. For our purpose, we think it is valid to look for causes with higher
responsibility first (fewer variables to negate or fix) and favor them over
smaller causes. For example, if an effect has two actual causes: one with $2$
variables in $\vec{X}$, $3$ in $\vec{W}$, and the second with $1$ variable in
$\vec{X}$, $5$ in $\vec{W}$, we pick the first. That said, we still want to
distinguish between $\vec{X}$ and $\vec{W}$ in causes with the same $dr$.
Assume we have two causes: the first with $2$ variables in $\vec{X}$, $3$ in
$\vec{W}$, and the second with $3$ in $\vec{X}$, $2$ in $\vec{W}$. Although
both are optimal solutions to $objective_{1}$, we would like to pick the one
with fewer causes. Thus, we add $objective_{2}$ to minimize causes, i.e., the
number of variables with $C^{1}$ and $C^{2}$ equal to $0$. We use hierarchical
objectives in ILP, for which the solver finds optimal solution(s) based on the
first objective, and then use the second objective to optimize the
solution(s).

We wrap-up with Algorithm 2, which omits the construction of $G^{*}$. We start
by turning $G^{*}$ into linear constraints in Line 3. The first objective
$\textit{obj}_{1}$, which maximizes $dr$ by maximizing the sum of $C^{1}_{i}$
is added in Line 4. The second objective, $\textit{obj}_{2}$, handles
minimizing the size of the cause set.

Algorithm 2 Causality Inference using $ILP_{why}$

1:causal model $M$, context $\langle U_{1},\ldots,U_{n}\rangle=\langle
u_{1},\ldots,u_{n}\rangle$, effect $\varphi$, evaluation $\langle
V_{1},\ldots,V_{m}\rangle=\langle v_{1},\ldots,v_{m}\rangle$

2:function FindCause($M,\vec{U}=\vec{u},\varphi,\vec{V}=\vec{v}$)

3: $\langle Con_{1},\ldots Con_{n}\rangle=$
$\textit{convertToILP}(\textit{CNF}(G^{*}))$

4:
$\textit{obj}_{1}=Maximize\;\sum_{i=1}^{m}C^{1}_{i}\;s.t.\;\textit{obj}_{1}\leq|\vec{V}|$

5:
$\textit{obj}_{2}=Minimize\;\sum_{i=1}^{m}(1-C^{1}_{i})*(1-C^{2}_{i})\;s.t.\;|\vec{V}|\geq\textit{obj}_{2}\geq
1$

6: if $\langle V_{1}=v_{1}^{\prime}\ldots
V_{m}=v_{m}^{\prime},C^{1}_{1}=c^{1}_{1}\ldots
C^{1}_{m}=c^{1}_{m},C^{2}_{1}=c^{2}_{1}\ldots C^{2}_{m}=c^{2}_{m}\rangle$
$\hookrightarrow$
$=\textit{solve}(\vec{Con},\textit{obj}_{1},\textit{obj}_{2})$ then

7: $\vec{X^{\prime}}\mathrel{\mathop{\mathchar 58\relax}}=\langle
X^{\prime}_{1}...X^{\prime}_{obj_{2}}\rangle$ s.t. $\forall i\forall
j\bullet(i\not=j\Rightarrow$
$X^{\prime}_{i}\not=X^{\prime}_{j})\wedge(X^{\prime}_{i}=V_{j}\Leftrightarrow\neg
c^{1}_{j}\wedge\neg c^{2}_{j})$

8: $\vec{W}\mathrel{\mathop{\mathchar 58\relax}}=\langle W_{1}...W_{s}\rangle$
s.t. $\forall i\forall j\bullet(i\not=j\Rightarrow$
$W_{i}\not=W_{j})\wedge(W_{i}=V_{j}\Leftrightarrow(\neg c^{1}_{j}\wedge
c^{2}_{j}))$

9: return $\vec{X^{\prime}},\vec{W}$

10: else return infeasible

11: end if

12:end function

We process the results after solving the program in Lines 6-8. The feasibility
of the program means we found a cause (size $\textit{obj}_{2}$) with the
maximum $dr$ for the effect. For the details, we check the indicators of each
variable. The cause is composed of variables that have $C^{1}$ and $C^{2}$
equal $0$; variables in $\vec{W}$, have $C^{1}=0$ and $C^{2}=1$.

Throwing rocks Example. Assume we want to answer why did the bottle shatter
$BS=1$? (given both threw). The generated program is not shown, but it was
solved with ($obj_{1}=2$), i.e., two normal variables, and $obj_{2}=1$, one
cause variable. Based on the indicators, $SH=1$ is the actual cause of $BS=1$,
given that $BH=0$. This is the result of having $C^{1}_{SH}=0\wedge
C^{2}_{SH}=0$ as opposed to $C^{1}_{BH}=0\wedge C^{2}_{BH}=1$. The result is
correct; $SH$ is a cause of $BS$, with the maximum $dr$. Previous references
of this example concluded $ST$ as a cause; however, since $SH$ is an identity
function, this does not compromise our result. 333Arguably, the (geodesic)
distance between the cause and effect nodes in the graph, can be taken into
consideration. In this paper, we do not consider this issue

##  4 Evaluation

To evaluate their efficiency, we implemented our strategies as an open-source
library. We used state of the art solvers: Gurobi [11] for ILP, and Open-WBO
for MaxSAT [27]. In this section, we evaluate the performance, in terms of
execution time and memory allocation, of the strategies in comparison with
previous work.

Experiment Setup Unfortunately, there are no standard data-sets to benchmark
causality computations. Thus, we gathered a dataset of $37$ models, which
included $21$ small models ($\leq 400$ endogenous variables)–from domains of
causality, security, safety, and accident investigation– and $16$ larger
security models from an industrial partner, in addition to artificially
generated models. The smaller models contained $9$ illustrative examples from
literature (number of endogenous variables in brackets) such as
$\mathit{Throwing-Rocks(5)}$, $\mathit{Railroad(4)}$ [12], $2$ variants of a
safety model that describes a leakage in a subsea production system
$\mathit{LSP(41)}$ and $\mathit{LSP2(41)}$ [7], and an aircraft accident model
(Ueberlingen, 2002) $\mathit{Ueb(95)}$ [34], $7$ generated binary tress, and a
security model obtained from an industrial partner which depicts how insiders
within a company steal a master encryption key $\mathit{SMK}$. Because it can
be parameterized by the number of employees in a company, we have $14$
variants of $\mathit{SMK}$, $2$ small ones $\mathit{SMK1(36)}$ and
$\mathit{SMK8(91)}$, and $12$ large models of sizes ($550-7150$). In addition,
we artificially generated $4$ models: $2$ binary trees with different heights,
denoted as $\mathit{BT(2047-4095)}$, and $2$ trees combined with non-tree
random models, denoted as $\mathit{ABT(4103)}$, and $\mathit{ABT2(8207)}$. We
have evidence that such large models are likely to occur when built
automatically from architectures or inferred from other sources [17, 16].
Details on the models and the results can be found online.444Machine-readable
models and their description available at https://git.io/Jf8iH

We formulated a total of $\mathbf{484}$ checking queries that vary in the
context, cause, effect, and consequently differ in the result of AC1-AC3, the
size of $\vec{W}$, and the size of the minimal cause. For the smaller models,
we specified the queries manually according to their sources in literature,
and verified that our results match the sources. The approaches, including
previous ALL-SAT approach, answered these queries in under a second; hence, we
exclude them from our discussion. For the larger models we constructed a total
of $\mathbf{224}$ checking queries. We specified some effects (e.g., root of
$\mathit{BT}$, or steal pass phrase in $\mathit{SMK}$) and used different
contexts, and randomly selected causes (sizes 1, 2, 3, 4, 10, 15, and 50) from
the models. Since we can reuse the checking queries for inference by omitting
the cause, we created $\mathbf{180}$ inference queries including $\mathbf{67}$
query of large models.

We collected the results for: SAT \- the original SAT-based approach [18], and
the presented three approaches: ILP, MaxSAT, and ILP${}_{\texttt{why}}$\- the
inference approach. We ran each query for $30$ warm-ups (dry-runs before
collecting results to avoid accounting for factors like JVM warm-up), and $30$
measurement iterations on an i7 Ubuntu machine with $16$ GB RAM. We set the
cut-off threshold to $2$ hours.

Discussion. Generally, we use cactus plots to compare the performance of the
approaches. The x-axis shows the number of queries an approach answered
ordered by the execution time, which is shown on the y-axis; a point ($x,y$)
on the plot reads as $x$ queries can be answered in $y$ or less. Next, we
discuss the overall trends of the results; however, since we are interested in
notions of checking, and inference, we also mention specific queries in which
AC3 does not hold.

As expected, the experiments confirmed the problems with the SAT encoding—
significant solver slow-down and memory exhaustion—[35]. Thus, as shown in
1(a), SAT only answered $\mathbf{187}$ of the $\mathbf{224}$ checking queries;
for the remaining either it ran out of memory or took more than $2$ hours. For
instance, queries on $\mathit{SMK(6600)}$ checking causes of sizes $2,3,4$
were not answered because the program ran out of memory. With almost all
answered queries, SAT took al least two to four times as much as ILP, and up
to twenty times as much as MaxSAT. In extreme cases, SAT took around $113$
minutes to finish, whereas others stayed under $5s$ for the same cases. Memory
allocation, shown in 1(b), was similar to the execution time. However, it
showed less difference with ILP and sometimes better allocation. Although it
is not surprising that an ALL-SAT encoding performs poorly in some situations,
the key result is that both ILP and MaxSAT provide more informative answers to
a query while performing better.

According to our dataset, both ILP and MaxSAT, answered all queries in less
than $70-100$ seconds. Especially for semi-inference, cases of non-minimal
causes and a minimal cause can be found, they are effective. For instance,
with queries using $\mathit{ABT(4103)}$, we found causes of size $2$, $5$, and
$11$ out of candidate causes of sizes $5$, $10$, $15$, and $50$. All these
queries were answered in around $5s$ using ILP, and $2s$ using MaxSAT. For
larger and more complex models e.g., $\mathit{SMK(7150)}$, answering similar
queries jumped to $98s$ with ILP and $71s$ MaxSAT.

As shown in 1(a) and 1(b), MaxSAT outperformed ILP in execution time and
memory; a scatter plot to compare them is shown in 1(c). The propositional
nature of the problem gives an advantage to MaxSAT. Especially for easier
queries, as shown in 1(c) bottom left, MaxSAT is much faster because no linear
transformation is needed, which explains why the gap between the two decreases
among the larger queries. Further, we used Open-WBO —a solver that uses cores
to initiate (UN)SAT instances [27]— which performs better, especially when the
number of hard clauses is high [3]. That said, in addition to the comparison,
we used ILP for binary computations to incorporate quantifiable notions to
infer causality using multi-objective ILP in ILP${}_{\texttt{why}}$.

050100150200250Queries255075100125150175200CPU time (s)MaxSATILPSAT

(a) Cactus Plot of Execution Time

050100150200250Queries2571012151720Memory Allocation (GB)MaxSATILPSAT

(b) Cactus Plot of Memory Allocation

$\displaystyle 10^{0}$$\displaystyle 10^{1}$$\displaystyle
10^{2}$$\displaystyle 10^{3}$$\displaystyle 10^{4}$MaxSAT$\displaystyle
10^{0}$$\displaystyle 10^{1}$$\displaystyle 10^{2}$$\displaystyle
10^{3}$$\displaystyle 10^{4}$ILP1000 sec. timeout1000 sec. timeout

(c) Log-log Scatter Plot of ILP vs MaxSAT

050100150200250Queries200400600800100012001400CPU time
(s)MaxSATILPSATILP${}_{\texttt{why}}$

(d) Cactus Plot including ILP${}_{\texttt{why}}$

Figure 1: Execution Time and Memory Results on the Larger Models

Although we have fewer inference queries ($67$), for comparison, we plot the
checking approaches with ILP${}_{\texttt{why}}$ in 1(d).
ILP${}_{\texttt{why}}$ answered $\mathbf{63}$ out of $\mathbf{67}$ queries. In
comparison, it was slower than the checking approaches. Still, it scaled to
large and complex queries. For instance, with basic tree models of $4000$
variables ($\mathit{BT_{11}}$, $\mathit{ABT}$), it took $8s$, and scaled to
$8000$ variable $\mathit{ABT2}$ within $63s$. However, it slowed down with
larger models with complex semantics, i.e., $\mathit{SMK}$ different variants.
For instance, $\mathit{SMK(5500)}$ took $280s$, while $\mathit{SMK(6600)}$
jumped to $1400s$. The slow down is related to the memory allocation because
the program, finally, ran out of memory with queries on $\mathit{SMK(7150)}$.
Given sufficient memory, we think ILP${}_{\texttt{why}}$ computes inference
for even larger models.

In summary, we argue that the three approaches efficiently automates actual
causality reasoning over binary models. Our MaxSAT encoding performs well for
purposes of causality checking and semi-inference. Although slower,
ILP${}_{\texttt{why}}$ is also efficient and scalable for purposes of
inference.

##  5 Related Work

There are three versions of HP (original 2001, updated 2005, modified 2015 )
[13]. We use the latest because it solves issues with the previous versions,
and reduces the complexity [12]. To the best of our knowledge, no previous
work tackled the implementation of the (modified) HP. Still, we discuss the
implementations of previous versions. Previous work has proposed simplified
adaptations of the definition for various applications. First, in the domain
of databases [28, 6, 33], (updated) HP was utilized to explain conjunctive
query results. The approaches heavily depend on the correspondence between
causes and domain-specific concepts such as lineage, database repairs, and
denial constraints. The simplification in that line of work is the limitation
to a single-equation causal model based on the lineage of the query in [28],
or no-equation model in [6, 33], in addition to the elimination of preemption
treatment. Similar simplification has been made for Boolean circuits in [9].
Second, in the context of software and hardware verification, (updated) HP is
used to explain counterexamples returned by a model checker [5]. The authors
also restricted the definition to singleton causes and no-equation models.
Third, in [4, 23], the authors adapted HP to debug models of safety-critical
systems. Similar to our approach, all the papers above use acyclic binary
models. However, they depend heavily on the correspondence between causes and
domain-specific concepts. Also, for efficiency, they relax the definition by
restricting the model, i.e., one equation[28], no-equations [6, 33, 5], or by
restricting the cause, i.e., singleton [5, 33]; the complexity is then
relaxed, because AC2 is straightforward (no $\vec{W}$) or AC3 is not needed.
While such limitations are sufficient for the particular use-case, we argue
that they cannot be used outside their respective domains, e.g., for
accountability. In contrast, our approach is a general method to automate HP.
We focus on the minimality, which, to the best of our knowledge, no previous
work has tackled. We employ optimization solving, which was not utilized
before in this context. Alternatively, previous work used SAT directly [18],
indirectly [4], or answer set programming [6]. Sharing our generality, Hopkins
proposed methods to check (original) HP using search-based algorithms [14].
Our approach scales to thousands of variables, while the results presented in
the search-based approaches showed a limit of 30 variables.

Fault tree analysis (FTA) is an established design-time method to analyze
safety risks of a system [32]. FTA’s primary analysis is the computation of
minimal cut sets MCSs of a fault tee; a CS is a set of events that, together,
cause the top-level event. Approaches to determine MCS use Boolean
manipulation, or Binary decision diagrams [32]. These methods are similar to
our computations; however, the conceptual difference is the definition of a
cause. While a cause covers two notions: sufficiency and necessity, a CS
presents a sufficient cause only. The occurrence of the events in the cut
leads to the occurrence of the top-level event. This roughly corresponds to
AC1, while the minimality of the cut set corresponds to AC3. The difference
lies in the necessity of the cause (AC2). An MCS computation does not include
this step, which is the core of actual causality computation. Cut sets are all
the enumerations that make the effect true. Similarly, model-based diagnosis
(MBD) aims to detect faulty components to explain anomalies in system behavior
[31]. The model is a set of logical expressions over a set of components. MBD
requires a set of observations that correspond to the context $\vec{U}$; using
logical inference, MBD outputs a set of hypotheses for how the system differs
from its model, i.e., diagnoses. While MBD can be considered as an approach to
infer causality, it does not require counterfactuality of the cause. Although
MBD uses a notion of intervention (setting some components to abnormal), this
is not counterfactual reasoning. Instead, it is a sufficiency check since MBD
uses a behavioral model, i.e., a representation of the correct behavior. Like
FTA, diagnoses are sufficient causes, but not actual causes.

##  6 Conclusions and Future Work

According to HP, a set of events ($\vec{X}$) causes an effect ($\varphi$) if
(1) both actually happen; (2) changing some values of $\vec{X}$ while fixing a
set $\vec{W}$ of the remaining variables at their original value leads to
$\varphi$ not happening; and (3) $\vec{X}$ is minimal. The complexity of the
general problem has been established elsewhere. We show that when restricting
to binary models, the problem of checking or inferring causality can
effectively and efficiently be solved as an optimization problem. The problem
is not trivial because intuitively, we need to enumerate all sets $\vec{W}$
from condition (2) and need to check minimality for condition (3). We show how
to formulate both properties as an optimization problem instead which
immediately gives rise to using a solver to determine if a cause satisfies all
conditions, or find one that does. For that, we define an objective function
that encodes the distance between cause values in the actual and
counterfactual worlds. If we now manage to optimize the problem with a smaller
cause, then we know that it satisfies condition (2) but is not minimal. With
an additional objective to quantify responsibility, we also formulate
inference as an optimization problem. Using models with $8000$ variables,
which we deem realistic and necessary for automatically inferred causal
models, we show that our approaches answer checking queries in seconds, and
inference queries in minutes. In the future, we plan to explore the extension
of the approach to support non-binary models.

## References

  * [1] Aleksandrowicz, G., Chockler, H., Halpern, J.Y., Ivrii, A.: The computational complexity of structure-based causality. In: Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence (2014)
  * [2] Bacchus, F., Järvisalo, M., Martins, R., et al.: MaxSAT evaluation 2018 (2018)
  * [3] Bacchus, F., Narodytska, N.: Cores in core based MaxSAT algorithms: An analysis. In: International Conference on Theory and Applications of Satisfiability Testing
  * [4] Beer, A., Heidinger, S., Kühne, U., Leitner-Fischer, F., Leue, S.: Symbolic causality checking using bounded model checking. In: Model Checking Software - 22nd International Symposium, SPIN (2015)
  * [5] Beer, I., Ben-David, S., Chockler, H., Orni, A., Trefler, R.J.: Explaining counterexamples using causality. Formal Methods in System Design 40(1), 20–40 (2012)
  * [6] Bertossi, L.: Characterizing and computing causes for query answers in databases from database repairs and repair programs. In: International Symposium on Foundations of Information and Knowledge Systems. pp. 55–76. Springer (2018)
  * [7] Cheliyan, A.S., Bhattacharyya, S.K.: Fuzzy fault tree analysis of oil and gas leakage in subsea production systems. Journal of Ocean Engineering and Science (2018)
  * [8] Chockler, H., Halpern, J.Y.: Responsibility and blame: A structural-model approach. J. Artif. Intell. Res. 22, 93–115 (2004). https://doi.org/10.1613/jair.1391
  * [9] Chockler, H., Halpern, J.Y., Kupferman, O.: What causes a system to satisfy a specification? ACM Transactions on Computational Logic (TOCL) 9(3), 20 (2008)
  * [10] Feigenbaum, J., Hendler, J.A., Jaggard, A.D., Weitzner, D.J., Wright, R.N.: Accountability and deterrence in online life. In: Web Science (2011)
  * [11] Gurobi Optimization, L.: Gurobi optimizer reference manual (2018)
  * [12] Halpern, J.Y.: A modification of the Halpern-Pearl definition of causality. In: Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI. pp. 3022–3033 (2015)
  * [13] Halpern, J.Y.: Actual causality. The MIT Press, Cambridge, Massachussetts (2016)
  * [14] Hopkins, M.: Strategies for determining causes of events. In: AAAI/IAAI (2002)
  * [15] Hume, D.: An Enquiry Concerning Human Understanding (1748)
  * [16] Ibrahim, A., Kacianka, S., Pretschner, A., Hartsell, C., Karsai, G.: Practical causal models for cyber-physical systems. In: NASA Formal Methods. pp. 211–227 (2019)
  * [17] Ibrahim, A., Klesel, T., Zibaei, E., Kacianka, S., Pretschner, A.: Actual causality canvas: A general framework for explanation-based socio-technical constructs. In: ECAI 2020, the 24th European Conference on Artificial Intelligence. Frontiers in Artificial Intelligence and Applications, IOS Press (2020)
  * [18] Ibrahim, A., Rehwald, S., Pretschner, A.: Efficient checking of actual causality with sat solving. Engineering Secure and Dependable Software Systems 53, 241 (2019)
  * [19] Kacianka, S., Ibrahim, A., Pretschner, A., Trende, A., Lüdtke, A.: Extending causal models from machines into humans. Electronic Proceedings in Theoretical Computer Science 308, 17–31 (2019). https://doi.org/10.4204/eptcs.308.2
  * [20] Koch, T., Martin, A., Pfetsch, M.E.: Progress in academic computational integer programming. In: Facets of Combinatorial Optimization. Springer (2013)
  * [21] Künnemann, R., Esiyok, I., Backes, M.: Automated verification of accountability in security protocols. CoRR abs/1805.10891 (2018)
  * [22] Ladkin, P., Loer, K.: Why-because analysis: Formal reasoning about incidents. Bielefeld, Germany, Document RVS-Bk-98-01, Technischen Fakultat der Universitat Bielefeld, Germany (1998)
  * [23] Leitner-Fischer, F., Leue, S.: Causality checking for complex system models. In: Verification, Model Checking, and Abstract Interpretation, 14th International Conference, VMCAI 2013, Rome, Italy, January 20-22, 2013. Proceedings (2013)
  * [24] Lewis, D.: Causation. Journal of Philosophy 70(17), 556–567 (1973)
  * [25] Li, C.M., Manyà, F.: MaxSAT, hard and soft constraints. In: Handbook of Satisfiability, pp. 613–631 (2009)
  * [26] Li, R., Zhou, D., Du, D.: Satisfiability and integer programming as complementary tools. In: Proceedings of the 2004 Asia and South Pacific design automation conference. pp. 879–882. IEEE Press (2004)
  * [27] Martins, R., Manquinho, V., Lynce, I.: Open-WBO: A modular MaxSAT solver. In: International Conference on Theory and Applications of Satisfiability Testing. pp. 438–445. Springer (2014)
  * [28] Meliou, A., Gatterbauer, W., Halpern, J.Y., Koch, C., Moore, K.F., Suciu, D.: Causality in databases. IEEE Data Eng. Bull. 33(3), 59–67 (2010)
  * [29] Miller, T.: Explanation in artificial intelligence: Insights from the social sciences. Artificial Intelligence (2018)
  * [30] Pearl, J.: Causation, action and counterfactuals. In: Proceedings of the Sixth Conference on Theoretical Aspects of Rationality and Knowledge. pp. 51–73 (1996)
  * [31] Reiter, R.: A theory of diagnosis from first principles. Artificial intelligence (1987)
  * [32] Ruijters, E., Stoelinga, M.: Fault tree analysis: A survey of the state-of-the-art in modeling, analysis and tools. Computer science review 15, 29–62 (2015)
  * [33] Salimi, B., Bertossi, L.: From causes for database queries to repairs and model-based diagnosis and back (2014)
  * [34] Stuphor, J.: WBG of the 2002 Überlingen Mid-Air Collision, https://rvs-bi.de/Bieleschweig/5.5/Stuphorn˙Ueberlingen˙WBA.pdf
  * [35] Zhao, W., Wu, W.: ASIG: an all-solution SAT solver for CNF formulas. In: 11th International Conference on Computer-Aided Design and Computer Graphics

##  Appendix 0.A Proofs

In this section, we present proof sketches of the theorems in the paper.

###  0.A.1 Theorem 2 Proof Idea

Before presenting the proof of Subsection 3.1, we present 1. Recall that
Formula $F$ is constructed as follows.

$\displaystyle F\mathrel{\mathop{\mathchar
58\relax}}=\neg\varphi\wedge\bigwedge\limits_{i=1\ldots
n}f(U_{i}=u_{i})\wedge\bigwedge\limits_{i=1\ldots m,\not\exists j\bullet
X_{j}=V_{i}}\left(V_{i}\leftrightarrow F_{V_{i}}\lor
f(V_{i}=v_{i})\right)\wedge\bigwedge\limits_{i=1\ldots\ell}f(X_{i}=\neg
x_{i})$ (4)

###### Lemma 1

Formula $F$ constructed in Equation 4 is satisfiable iff AC2 holds for a given
model $M$, context $\vec{u}$, candidate cause $\vec{X}$, and effect $\varphi$.

###### Proof

The proof consists of two parts.

###### Part 1

SAT($F$) $\implies$ AC2, AC2 holds if $F$ is satisfiable

We show this by contradiction. Assume that $F$ is satisfiable and AC2 does not
hold. Based on $F$’s truth assignment, $\vec{v^{\prime}}$, we cluster the
variables into:

1. $\vec{X}$: each variable is fixed exactly to the negation of its original value, i.e., $X_{i}=\neg x_{i}\forall X_{i}\in\vec{X}$ (recall $\vec{X}\subseteq\vec{V}$). 2. $\vec{W}^{*}$: variables in this group, if they exist, have equal truth and original assignments, i.e., $\langle W^{*}_{1},\ldots,W^{*}_{s}\rangle$ s.t. $\forall i\forall j\bullet(i\not=j\Rightarrow W^{*}_{i}\not=W^{*}_{j})\wedge(W^{*}_{i}=V_{j}\Leftrightarrow v_{j}^{\prime}=v_{j})$ 3. $\vec{Z}$: variables in this group evaluate differently from their original evaluation, i.e., $\langle Z_{1},\ldots,Z_{k}\rangle$ s.t. $\forall i\forall j\bullet(i\not=j\Rightarrow Z_{i}\not=Z_{j})\wedge(Z_{i}=V_{j}\Leftrightarrow v_{j}^{\prime}\not=v_{j})\wedge(\forall i\not\exists j\bullet Z_{i}=X_{j}$).

Using $\vec{W^{*}},\vec{Z}$, we re-write $F$ as $F^{\prime}$ which is also
satisfiable.

Recall that $M$ is acyclic; therefore there is a unique solution to the
equations. Let $\Psi$ be the equations in $M$ without the equations that
define the variables $\vec{X}$. Let $\Psi_{k}$ be $\Psi$ without the equations
of some variables in a set $\vec{W_{k}}$. Since AC2 does not hold, $\forall
k\bullet\vec{W_{k}}\subseteq V\setminus X\Rightarrow(\vec{X}=\vec{\neg
x}\wedge\vec{W_{k}}=\vec{w_{k}}\wedge\Psi_{k}\wedge\neg\varphi)$ evaluates to
false. In case $\vec{W_{k}}=\vec{W^{*}}$, the previous unsatisfiable formula
is equivalent to the satisfiable $F^{\prime}$, implying a contradiction.

###### Part 2

AC2 $\implies$ SAT($F$); $F$ is satisfiable if AC2 holds

Assume that AC2 holds and $F$ is unsatisfiable. Then
$\exists\vec{W},\vec{w},\vec{x}^{\prime}\bullet(M,\vec{u})\models(\vec{W}=\vec{w})\implies(M,\vec{u})\models\bigl{[}\vec{X}\leftarrow\vec{x}^{\prime},\vec{W}\leftarrow\vec{w}\bigr{]}\neg\varphi$.
By definition [12], $(M,\vec{u})\models[Y_{1}\leftarrow y_{1}..Y_{k}\leftarrow
y_{k}]\varphi$ is equivalent to $(M_{Y_{1}\leftarrow y_{1}..Y_{k}\leftarrow
y_{k}},\vec{u})\models\varphi$, i.e., we replace specific equations in $M$ to
obtain a new model $M^{\prime}=M_{Y_{1}\leftarrow y_{1},...,Y_{k}\leftarrow
y_{k}}$. So,we replace the equations of the variables in $\vec{X},\vec{W}$ in
$M$ to obtain a new model, $M^{\prime}$, such that
$(M^{\prime},\vec{u})\models\neg\varphi$. Equations of $\vec{X},\vec{W}$
variables are now of the form $V_{i}=v_{i}$, i.e., each variable is equal to a
constant value. Note that $M^{\prime}$ is only different from $M$ in the
equations of $\vec{X},\vec{W}$. Hence, $M^{\prime}$ is acyclic and has a
unique solution for a given $\vec{U}=\vec{u}$. We construct a formula,
$F^{\prime}$ (shown below), that is a conjunction of the variables in sets
$X^{\prime},W^{\prime},U$ in $M^{\prime}$. Because of their equations, each
variable is represented by a constant, i.e., a positive or a negative literal.
Based on the nature of this formula, it is satisfiable with exactly the same
truth assignment as the unique solution of $M^{\prime}$.

$\displaystyle F^{\prime}\mathrel{\mathop{\mathchar
58\relax}}=\bigwedge_{i=1\ldots n}f(U_{i}=u_{i})\wedge\bigwedge_{i=1\ldots
s}f(W_{i}^{\prime}=w_{i}^{\prime})\wedge\bigwedge_{i=1\ldots\ell}f(X_{i}^{\prime}=x_{i}^{\prime})$

Now, we add the remaining variables, i.e., $\forall i\bullet
V_{i}\notin(\vec{X}\cup\vec{W})$, as formulas using the $\leftrightarrow$
operator. The overall formula $F^{\prime\prime}$, is satisfiable because we
have an assignment that makes each equivalence relation true.

$\displaystyle F^{\prime\prime}\mathrel{\mathop{\mathchar
58\relax}}=F^{\prime}\wedge\bigwedge_{i=1\ldots m,\not\exists j\bullet
X_{j}=V_{i},W_{j}=V_{i}}(V_{i}\leftrightarrow F_{V_{i}})$

We have $(M^{\prime},\vec{u})\models\neg\varphi$, which says that the model
evaluates $\neg\varphi$ to true with its unique solution (same assignment of
$F^{\prime\prime}$). We add another clause to $F^{\prime\prime}$ which
evaluates to true and keeps the formula satisfiable. That is,
$F^{\prime\prime\prime}\mathrel{\mathop{\mathchar
58\relax}}=F^{\prime\prime}\wedge\neg\varphi$. Last, we only have to show the
relation between ($F$ and $F^{\prime\prime\prime}$). We can rewrite $F$ (shown
at the beginning of the proof) such that we remove all disjuncts of the form
$(V_{i}\leftrightarrow F_{V_{i}})$ for the variables in $\vec{W}$. Similarly,
we remove all disjuncts of the form $f(V_{i}=v_{i})$ for all the variables
that are not in $\vec{W}$. According to our assumption, $F$ is still
unsatisfiable, since we removed disjunctions from the clauses. Then, we reach
a contradiction since $F$ is equivalent to $F^{\prime\prime\prime}$ which is
satisfiable for the same clauses.

###### Theorem LABEL:ilp

###### Proof

The proof follows form the remark that $G$, which both formulations are based
on, is a generalization of $F$ and is satisfiable if the context $\vec{U}$
makes $\varphi$ evaluate to its negation, given that the semantics of the
model is expressed using the constraints added, and the cause set, $\vec{X}$,
is not constrained to have other values ($\vec{x^{\prime}}$). We show this in
the following:

  1. 1.

Recall $G\mathrel{\mathop{\mathchar
58\relax}}=\neg\varphi\wedge\bigwedge_{i=1\ldots\ell}f(U_{i}=u_{i})\wedge\bigwedge_{i=1\ldots
m,\not\exists j\bullet X_{j}=V_{i}}(V_{i}\leftrightarrow F_{V_{i}}\lor
f(V_{i}=v_{i}))\wedge\bigwedge_{i=1\ldots\ell}(X_{i}\lor\neg X_{i})$. Rewrite
the formula to abstract the first part as, $G\mathrel{\mathop{\mathchar
58\relax}}=G_{base}\wedge\bigwedge_{i=1\ldots n}(X_{i}\lor\neg X_{i})$.

  2. 2.

Note how $\vec{X_{(n)}}$ is added to $G$ as $(X_{1}\vee\neg
X_{1})\wedge(X_{2}\vee\neg X_{2})\dots(X_{n}\vee\neg X_{n})$. Re-write this
big conjunction to its equivalent disjunctive normal from (DNF) i.e., $(\neg
X_{1}\wedge\neg X_{2}\dots\wedge\neg X_{n})\lor(\neg X_{1}\wedge\neg
X_{2}\dots\wedge X_{n})\dots\lor(X_{1}\wedge X_{2}\dots\wedge X_{n})$. Assume
wlog that all the actual values of $\vec{X_{(n)}}$ were true, hence to check
them in AC2 we need to have their values negated, i.e., $\neg X_{i}$. Looking
at the DNF, we have $2^{n}$ clauses that list all the possible cases of
negating or fixing the elements in $\vec{X}$. Then, we partition $G$ according
to the clauses, i.e, $G\mathrel{\mathop{\mathchar 58\relax}}=G_{1}\lor
G_{2}\dots G_{2^{n}}$, where $G_{1}\mathrel{\mathop{\mathchar
58\relax}}=G_{base}\wedge(\neg X_{1}\wedge\neg X_{2}\dots\wedge\neg X_{n})$.
$G_{1}$, is formula $F$ for $\vec{X}$, which according to 1 is satisfiable iff
AC2 holds for $\vec{X}$. $G$ holds if any $G_{i}$ hold.

  3. 3.

Generally $G_{i}$, fixes some (possibly none) elements to their original
evaluation ($X_{i}$) and negates some, possibly none ($G_{2^{n}}$), other
elements ($\neg X_{i}$). $G_{i}$ is an $F$ formula (from Equation 4) for the
negated variables, in a clause, as $\vec{X}$ but with some special fixed
variables that are added to $\vec{W}$. Based on 1 $G_{i}$ is satisfiable iff
AC2 for a the subset of the causes given that the other part (fixed) of the
cause is in $\vec{W}$, holds. Thus $G$ is satisfiable if AC2 holds for any
subset of it.

  4. 4.

The transformation from $G$ to an ILP program $P$ is proved to be correct
[26]. This means that satisfiability of $G$ entails feasibility of $P$. $P$ is
then feasible if AC2 holds for the A.) whole $\vec{X}$, B.) parts of
$\vec{X}$, or C.) an empty set of causes. Adding the distance constraint to
$P$ results in a new program $P^{\prime}$. Recall that the distance will be
the count of variables $\in\vec{X}$ that have a value $\vec{x^{\prime}}$ in
the solution of $P^{\prime}$. The distance should be greater than 0, i.e.,
case C is treated. By its nature, the ILP solver will pick the solution set
that makes the distance the least. Hence, if $\vec{X}$ is minimal in
fulfilling AC2 it will be picked, i.e., case A. Similarly case B is treated.

  5. 5.

Similarly, since $G$ forms the hard clauses of the MaxSat $G_{max}$, then
$G_{max}$ is satisfiable if $G$ is satisfiable. $G_{max}$ is then satisfiable
if AC2 holds for the A.) whole $\vec{X}$, B.) parts of $\vec{X}$, or C.) an
empty set of causes. We get rid of (C) by adding $K$ clause as a hard clause.
As such, $G_{max}$ is satisfiable only when for cases A and B.

###  0.A.2 Inference Proofs

###### Theorem LABEL:why

###### Proof

The proof follows from the correspondence between formula $G^{*}$ and $F$. The
proof consists of two parts.

###### Part 1

SAT($G^{*}$) $\implies$ $\exists\vec{X}$ such that AC2 holds for $\vec{X}$

We show this by contradiction. Assume that $G^{*}$ is satisfiable and
$\not\exists\vec{X}$ such that AC2 holds.

  1. 1.

$G^{*}\mathrel{\mathop{\mathchar
58\relax}}=\neg\varphi\wedge\bigwedge_{i=1\ldots
n}f(U_{i}=u_{i})\wedge\bigwedge_{i=1\ldots
m}\left(\left(\left(V_{i}\leftrightarrow F_{V_{i}}\right)\land
C^{1}_{i}\right)\lor\left(\neg\left(V_{i}\leftrightarrow
F_{V_{i}}\right)\land\neg C^{1}_{i}\right)\right)\\\
\land\left(\left(V_{orig}\land C^{2}_{i}\right)\lor\left(\neg
V_{orig}\land\neg C^{2}_{i}\right)\right)$

  2. 2.

For readability let us call $\left(V_{i}\leftrightarrow F_{V_{i}}\right)$ as
$e_{i}$. Since $G^{*}$ is satisfiable, every conjunction $CON_{i}$:
$\left(\left(e_{i}\land C^{1}_{i}\right)\lor\left(\neg e_{i}\land\neg
C^{1}_{i}\right)\right)\land\left(\left(V_{orig}\land
C^{2}_{i}\right)\lor\left(\neg V_{orig}\land\neg C^{2}_{i}\right)\right)$
holds. It is a matter of natural deduction to show that when $CON_{i}$ holds
with values $(C^{1}_{i}\lor C^{2}_{i})$ ($01,10,11$) it implies $e_{i}\lor
V_{orig}$, that is proving the following proposition $((e_{i}\land
C^{1}_{i})\lor(\neg e_{i}\land\neg C^{1}_{i}))\land((V_{orig}\land
C^{2}_{i})\lor(\neg V_{orig}\land\neg C^{2}_{i})))\land(C^{1}_{i}\lor
C^{2}_{i})\implies e_{i}\lor V_{orig}$. The only remaining case of
$(C^{1}_{i}C^{2}_{i})$ is $00$. This case, in turn, implies $\neg
e_{i}\land\neg V_{orig}$. That is the proposition: $((e_{i}\land
C^{1}_{i})\lor(\neg e_{i}\land\neg C^{1}_{i}))\land((V_{orig}\land
C^{2}_{i})\lor(\neg V_{orig}\land\neg C^{2}_{i}))\land(\neg C^{1}_{i}\land\neg
C^{2}_{i})\implies\neg e_{i}\land\neg V_{orig}$ can be proved by deduction.
Note that there is no guarantee that the $(C^{1}_{i}C^{2}_{i})=00$ case always
exists (this case is handled by the algorithm).

  3. 3.

For each variable in $M$, adding the implications from above to a formula
$Y=\neg\varphi\wedge\bigwedge_{i=1\ldots n}f(U_{i}=u_{i})$ would result in an
$F$ formula (from Equation 4) for some $\vec{X}$. $Y$ is satisfiable which by
1 makes AC2 holds for $\vec{X}$. This contradicts with the first assumption.

###### Part 2

$\exists\vec{X}$ such that AC2 holds for $\vec{X}$ $\implies$ SAT($G^{*}$)

We show this by contradiction, as well. Assume $\exists\vec{X}$ such that AC2
holds, and that $G^{*}$ is un-satisfiable. Since AC2 holds then there exists a
stisfiable $F$ as constructed in Equation 4. Similar to the first part of the
proof, since each variable $V_{i}$ has a satisfiable conjunction in $F$, it
implies a conjuntion in $G^{*}$ (the inverse of the implications in the first
part (without $C^{1}_{i},C^{2}_{i}$)). With that $G^{*}$ is satisfiable. This
contradiction proves the second part of the theorem.