Efficiently Checking Actual Causality with SAT Solving
Recent formal approaches towards causality have made the concept ready for incorporation into the technical world. However, causality reasoning is computationally hard; and no general algorithmic approach exists that efficiently infers the causes for effects. Thus, checking causality in the context of complex, multi-agent, and distributed socio-technical systems is a significant challenge. Therefore, we conceptualize an intelligent and novel algorithmic approach towards checking causality in acyclic causal models with binary variables, utilizing the optimization power in the solvers of the Boolean Satisfiability Problem (SAT). We present two SAT encodings, and an empirical evaluation of their efficiency and scalability. We show that causality is computed efficiently in less than 5 seconds for models that consist of more than 4000 variables.
Code (1)
Similar Papers 제목 키워드 기반
From Checking to Inference: Actual Causality Computations as Optimization Problems
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 …
counterfactualWhat Is a Counterfactual Cause in Action Theories?
Since the proposal by Halpern and Pearl, reasoning about actual causality has gained increasing attention in artificial intelligence, ranging from domains such as model-checking and verification to reasoning about action…
counterfactualCounterfactuals Modulo Temporal Logics
Lewis' theory of counterfactuals is the foundation of many contemporary notions of causality. In this paper, we extend this theory in the temporal direction to enable symbolic counterfactual reasoning on infinite sequenc…
counterfactualCounterfactual ReasoningHalf-checking propagators
Propagators are central to the success of constraint programming, that is contracting functions removing values proven not to be in any solution of a given constraint. The literature contains numerous propagation algorit…
Temporal Causal Reasoning with (Non-Recursive) Structural Equation Models
Structural Equation Models (SEM) are the standard approach to representing causal dependencies between variables in causal models. In this paper we propose a new interpretation of SEMs when reasoning about Actual Causali…
counterfactual