项目作者: amjadKhalifah

项目描述 :
A java library for actual causality computation.
高级语言: Java
项目地址: git://github.com/amjadKhalifah/HP2SAT1.0.git
创建时间: 2018-08-29T10:58:52Z
项目社区:https://github.com/amjadKhalifah/HP2SAT1.0

开源协议:MIT License

下载


Academic Citation

Please cite the following paper when using this tool.

Ibrahim, A., Rehwald, S., Pretschner, A.: Efficiently checking actual causality with sat solving. In: Dependable Software Systems Engineering (2019), https://arxiv.org/abs/1904.13101

@incollection{ibrahim2019,
author={Ibrahim, Amjad and Rehwald, Simon and Pretschner, Alexander},
title = {Efficiently Checking Actual Causality with SAT Solving},
booktitle = {Dependable Software Systems Engineering},
year = {2019},
url ={https://arxiv.org/abs/1904.13101},
}

hp2sat

Build Status

Background

This library allows to determine actual causality according to the modified Halpern-Pearl definition of causality [1]
. The used examples in the unit test cases (specifically in CausalitySolverInstanceTest) are described here.

Installation

Currently, this library is not published in a Maven repository. Please build it manually from source:

  1. $ mvn install

Then, you can import it using Maven:

  1. <dependency>
  2. <groupId>de.tum.in.i4</groupId>
  3. <artifactId>hp2sat</artifactId>
  4. <version>1.0</version>
  5. </dependency>

Alternatively, a pre-built .jar is offered in the release section of this repository.

Usage

General

Creation of a causal model

  1. // instantiate a new FormulaFactory
  2. FormulaFactory f = new FormulaFactory();
  3. // create exogenous variables; using _exo is not required, but used to distinguish them
  4. Variable BTExo = f.variable("BT_exo");
  5. Variable STExo = f.variable("ST_exo");
  6. // create endogenous variables; technically, there is no difference to exogenous ones
  7. Variable BT = f.variable("BT");
  8. Variable ST = f.variable("ST");
  9. Variable BH = f.variable("BH");
  10. Variable SH = f.variable("SH");
  11. Variable BS = f.variable("BS");
  12. // create the formula/function for each endogenous variable
  13. Formula BTFormula = BTExo;
  14. Formula STFormula = STExo;
  15. Formula SHFormula = ST;
  16. Formula BHFormula = f.and(BT, f.not(SH));
  17. Formula BSFormula = f.or(SH, BH);
  18. // create the equations of the causal model: each endogenous variable and its formula form an equation
  19. Equation BTEquation = new Equation(BT, BTFormula);
  20. Equation STEquation = new Equation(ST, STFormula);
  21. Equation SHEquation = new Equation(SH, SHFormula);
  22. Equation BHEquation = new Equation(BH, BHFormula);
  23. Equation BSEquation = new Equation(BS, BSFormula);
  24. Set<Equation> equations = new HashSet<>(Arrays.asList(BTEquation, STEquation, SHEquation,
  25. BHEquation, BSEquation));
  26. Set<Variable> exogenousVariables = new HashSet<>(Arrays.asList(BTExo, STExo));
  27. // instantiate the CausalModel
  28. CausalModel causalModel = new CausalModel("RockThrowing", equations, exogenousVariables, f);

Check whether ST = 1 is a cause of BS = 1 in the previously created causal model given ST_exo, BT_exo = 1 as context

  1. // IMPORTANT: Use the same FormulaFactory instance as in the above!
  2. /*
  3. * Create positive literals for ST_exo and BT_exo. If ST_exo, BT_exo = 0, we would create negative ones,
  4. * e.g. f.literal("ST_exo", false). Using f.variable("ST_exo") would be a shortcut for f.literal("ST_exo", true)
  5. */
  6. Set<Literal> context = new HashSet<>(Arrays.asList(f.literal("BT_exo", true),
  7. f.literal("ST_exo", true)));
  8. /*
  9. * Similar as for the context, we specify f.literal("ST", true) as cause and f.variable("BS") as phi, as we
  10. * want to express ST = 1 and BS = 1, respectively.
  11. */
  12. Set<Literal> cause = new HashSet<>(Collections.singletonList(f.literal("ST", true)));
  13. Formula phi = f.variable("BS");
  14. // finally, call isCause on the causal model using the SAT-based algorithm
  15. CausalitySolverResult causalitySolverResult =
  16. CauscausalModel.isCause(context, phi, cause, SolvingStrategy.SAT);

Use other algorithms

The SolvingStrategy enum contains all currently supported algorithms/strategies:

  1. public enum SolvingStrategy {
  2. BRUTE_FORCE, SAT, SAT_MINIMAL, SAT_COMBINED, SAT_COMBINED_MINIMAL,
  3. SAT_OPTIMIZED_AC3, SAT_OPTIMIZED_AC3_MINIMAL
  4. }

Just call the isCause-method with the respective SolvingStrategy:

  1. // Brute-Force
  2. CausalitySolverResult causalitySolverResult =
  3. CauscausalModel.isCause(context, phi, cause, SolvingStrategy.BRUTE_FORCE);
  4. // SAT-based
  5. CausalitySolverResult causalitySolverResult =
  6. CauscausalModel.isCause(context, phi, cause, SolvingStrategy.SAT);
  7. // SAT-based returning a minimal W for AC2
  8. CausalitySolverResult causalitySolverResult =
  9. CauscausalModel.isCause(context, phi, cause, SolvingStrategy.SAT_MINIMAL);
  10. // SAT-based where checking AC2 and AC3 is combined
  11. CausalitySolverResult causalitySolverResult =
  12. CauscausalModel.isCause(context, phi, cause, SolvingStrategy.SAT_COMBINED);
  13. // SAT-based where AC3 check does not require ALL-SAT
  14. CausalitySolverResult causalitySolverResult =
  15. CauscausalModel.isCause(context, phi, cause, SolvingStrategy.SAT_OPTIMIZED_AC3);

Important Notes

  • When working with a causal model, always use the same FormulaFactory instance. If not, an exception might occur.
  • When creating a CausalModel, it is checked whether the latter is valid. It needs to fulfill the following
    characteristics; otherwise an exception is thrown:
    • Each variable needs to be either exogenous or defined by exactly one equation.
    • The causal model must be acyclic. That is, no variables are allowed to mutually depend on each other
      (directly and indirectly)
    • Variables must not be named with "_dummy".

Literature

[1] J. Y. Halpern. “A Modification of the Halpern-Pearl Definition of Causality.” In: Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015. 2015, pp. 3022–3033.