Commit 3518f5b7 authored by Nikolai Käfer's avatar Nikolai Käfer 🏠
Browse files

version 0.7.1

parent 0f542be7
; P(cr⇒r) = 2 ∗ P(cr⇒m)
(declare-fun p_CR-R () Real)
(declare-fun p_CR-M () Real)
(assert (= p_CR-R (* 2 p_CR-M)))
; P(cr⇒r ∨ cr⇒m | cr) ≥ 0.98
; P((cr⇒r ∨ cr⇒m) ∧ cr) ≥ 0.98 ∗ P(cr)
; P(cr⇒r ∧ cr) + P(cr⇒m ∧ cr) ≥ 0.98 ∗ P(cr)
(declare-fun p_CR_CR-R () Real)
(declare-fun p_CR_CR-M () Real)
(declare-fun p_CR () Real)
(assert (>= (+ p_CR_CR-R p_CR_CR-M) (* 0.98 p_CR)))
; bicycle AF
CT ; continue
ST ; stop
; lidar
LD
LD-M
NLD
NLD-NM
; camera left
CL
CL-L
CL-M
NCL
NCL-NL
NCL-NM
; camera right
CR
CR-R
CR-M
NCR
NCR-NR
NCR-NM
# ; attacks
CT ST
LD NLD
LD NLD-NM
NLD LD
NLD LD-M
LD-M NLD-NM
LD-M NCL-NM
LD-M NCR-NM
LD-M CT
NLD-NM LD-M
NLD-NM CL-M
NLD-NM CR-M
CL NCL
CL NCL-NL
CL NCL-NM
NCL CL
NCL CL-L
NCL CL-M
CL-M NLD-NM
CL-M NCL-NM
CL-M NCR-NM
CL-M CT
NCL-NM LD-M
NCL-NM CL-M
NCL-NM CR-M
CL-L NCL-NL
NCL-NL CL-L
CR NCR
CR NCR-NR
CR NCR-NM
NCR CR
NCR CR-R
NCR CR-M
CR-M NLD-NM
CR-M NCL-NM
CR-M NCR-NM
CR-M CT
NCR-NM LD-M
NCR-NM CL-M
NCR-NM CR-M
CR-R NCR-NR
NCR-NR CR-R
\ No newline at end of file
; bicycle AF
CT ; continue
ST ; stop
; lidar
;LD
;LD-M
;NLD
;NLD-NM
; camera left
CL
CL-L
CL-M
NCL
NCL-NL
NCL-NM
; camera right
CR
CR-R
CR-M
NCR
NCR-NR
NCR-NM
# ; attacks
CT ST
;LD NLD
;LD NLD-NM
;NLD LD
;NLD LD-M
;LD-M NLD-NM
;LD-M NCL-NM
;LD-M NCR-NM
;LD-M CT
;NLD-NM LD-M
;NLD-NM CL-M
;NLD-NM CR-M
CL NCL
CL NCL-NL
CL NCL-NM
NCL CL
NCL CL-L
NCL CL-M
;CL-M NLD-NM
CL-M NCL-NM
CL-M NCR-NM
CL-M CT
;NCL-NM LD-M
NCL-NM CL-M
NCL-NM CR-M
CL-L NCL-NL
NCL-NL CL-L
CR NCR
CR NCR-NR
CR NCR-NM
NCR CR
NCR CR-R
NCR CR-M
;CR-M NLD-NM
CR-M NCL-NM
CR-M NCR-NM
CR-M CT
;NCR-NM LD-M
NCR-NM CL-M
NCR-NM CR-M
CR-R NCR-NR
NCR-NR CR-R
\ No newline at end of file
(declare-fun p_A1_nA2_B () Real)
(declare-fun p_A1_B () Real)
(assert (= p_A1_B 1))
\ No newline at end of file
A1
A2
B
C
#
A1 B
A1 A2
A2 B
A2 A1
B C
\ No newline at end of file
A
B
C
D
#
A B
B C
B D
D A
\ No newline at end of file
A
B
C
D
#
A B
;A D
B C
B D
C A
D B
\ No newline at end of file
A 0.5
B
C
D
#
A B
B C
C A
C D
D C
\ No newline at end of file
; P(A) = 2 ∗ P(C)
(declare-fun p_A () Real)
(declare-fun p_C () Real)
(assert (= p_A (* 2 p_C)))
; P(A ∨ C | -B) ≥ 0.8
; P((A ∨ C) ∧ -B) ≥ 0.8 ∗ P(-B)
; P(A ∧ -B) + P(C ∧ -B) - P(A ∧ C ∧ -B) ≥ 0.8 ∗ P(-B)
(declare-fun p_A_nB () Real)
(declare-fun p_nB_C () Real)
(declare-fun p_A_nB_C () Real)
(declare-fun p_nB () Real)
(assert (>= (- (+ p_A_nB p_nB_C) p_A_nB_C) (* 0.8 p_nB)))
\ No newline at end of file
; A and B attack each other, and B attacks C
A
B
C
#
A B
B A
B C
\ No newline at end of file
...@@ -6,7 +6,7 @@ CPrAA is a Python tool and package for various tasks in probabilistic abstract a ...@@ -6,7 +6,7 @@ CPrAA is a Python tool and package for various tasks in probabilistic abstract a
* find distributions satisfying numerous probabilistic argumentation semantics * find distributions satisfying numerous probabilistic argumentation semantics
* check for credulous or skeptical acceptance of arguments * check for credulous or skeptical acceptance of arguments
* maximize or minimize the marginal probability of certain arguments * maximize or minimize the marginal probability of certain arguments
* generate labellings according to different labelling schemes * generate labelings according to different labeling schemes
## Installation ## Installation
...@@ -99,15 +99,15 @@ The folder `AFs` contains a number of example argumentation frameworks in `.tgf` ...@@ -99,15 +99,15 @@ The folder `AFs` contains a number of example argumentation frameworks in `.tgf`
## Semantics ## Semantics
The semantics that should be enforced for a task are specified with the `--semantics` or `-s` flag. The semantics that should be enforced for a task are specified with the `--semantics` (or `-s`) flag.
There is also the option to specify that certain semantics should _not_ hold with `--complement_semantics` or `-cs`. There is also the option to specify that certain semantics should _not_ hold with `--complement_semantics` (or `-cs`).
A list of all available semantics can be viewed with `--list_semantics` or `-ls`: A list of all available semantics can be viewed with `--list_semantics` (or `-ls`):
$ cpraa --list_semantics $ cpraa --list_semantics
Available semantics: Min, Neu, Max, Dirac, Ter, Fou, SFou, Inv, Rat, Coh, Opt, SOpt, Jus, CF, WAdm, PrAdm, MinAdm, JntAdm, WCmp, PrCmp, MinCmp, JntCmp, ElmCF, ElmAdm, ElmCmp, ElmGrn, ElmPrf, ElmSStl, ElmStl, WNorS, NorS, SNorS, WNor, Nor, SNor, AF, NNorAF, NNor, CFs, StrengthCF, StrengthSupportCF, DiracCF, DiracAdm, DiracCmp, DiracGrn, DiracPrf, DiracSStl, DiracStl Available semantics: Min, Neu, Max, Dirac, Ter, Fou, SFou, Inv, Rat, Coh, Opt, SOpt, Jus, CF, WAdm, PrAdm, MinAdm, JntAdm, WCmp, PrCmp, MinCmp, JntCmp, ElmCF, ElmAdm, ElmCmp, ElmGrn, ElmPrf, ElmSStl, ElmStl, WNorS, NorS, SNorS, WNor, Nor, SNor, AF, NNorAF, NNor, CFs, StrengthCF, StrengthSupportCF, DiracCF, DiracAdm, DiracCmp, DiracGrn, DiracPrf, DiracSStl, DiracStl
Tip: With `--documentation` or `-d` followed by the names of one or more semantics a short description of most semantics is available: Tip: With `--documentation` (or `-d`) followed by the names of one or more semantics a short description of most semantics is available:
$ cpraa --documentation Fou MinAdm $ cpraa --documentation Fou MinAdm
Semantics 'Fou': Semantics 'Fou':
...@@ -176,9 +176,9 @@ As expected, the resulting distributions are the Dirac distributions of the assi ...@@ -176,9 +176,9 @@ As expected, the resulting distributions are the Dirac distributions of the assi
This task requires linear constraints and one or more arguments from the AF (passed with `--arguments` or `-a`). This task requires linear constraints and one or more arguments from the AF (passed with `--arguments` or `-a`).
If the constraints are satisfiable, the resulting distribution minimises (or respectively maximises) the marginal probability of the given argument, or, if multiple arguments are given, the probability of any argument holding. If the constraints are satisfiable, the resulting distribution minimises (or respectively maximises) the marginal probability of the given argument, or, if multiple arguments are given, the probability of any argument holding.
**Example:** (TODO) **Example:** Find a probabilistically complete distribution under which argument `B`'s marginal probability is maximal:
$ cpraa -f AFs\example.tgf --semantics PrCmp -a B -MAX $ cpraa -f AFs/example.tgf --semantics PrCmp -a B -MAX
Computing optimal distribution maximizing the probability of argument B while satisfying the following semantics: PrCmp Computing optimal distribution maximizing the probability of argument B while satisfying the following semantics: PrCmp
Support: Support:
P(-A, B,-C) = 1 P(-A, B,-C) = 1
...@@ -186,39 +186,162 @@ If the constraints are satisfiable, the resulting distribution minimises (or res ...@@ -186,39 +186,162 @@ If the constraints are satisfiable, the resulting distribution minimises (or res
### Acceptance checking for arguments ### Acceptance checking for arguments
`-CA`, `--credulous_acceptance` An argument `A` is _credulously accepted_ under some given constraints if at least one satisfying distribution exists with `P(A) = 1`, and _skeptically accepted_ if `P(A) = 1` holds for all distributions `P` that satisfy the constraints.
`-SA`, `--skeptical_acceptance` One or more arguments from the AF need to be specified following the `--arguments` (`-a`) flag to be checked with `--credulous_acceptance` (`-CA`) or `--skeptical_acceptance` (`-SA`).
As a shortcut, there is also `--credulous_acceptance_all` (`-CAA`) and `--skeptical_acceptance_all` (`-SAA`) to check credulous or skeptical acceptance for all arguments in the AF.
`-CAA`, `--credulous_acceptance_all` Acceptance checking is also possible with respect to a given threshold value, e.g., `t = 0.75`:
Then `A` is credulously accepted w.r.t. `t` if `P(A) >= 0.75` holds for at least one distribution, and likewise skeptically accepted w.r.t `t` if `P(A) >= 0.75` holds for all distributions.
Such a threshold can be specified directly following the flag for the respective acceptance checking task, e.g., `--credulous_acceptance 0.75`.
`-SAA`, `--skeptical_acceptance_all` **Example:** Check if argument `C` is skeptically accepted with a threshold of `0.5` under joint-complete semantics:
(TODO) $ cpraa -f AFs/example.tgf --semantics JntCmp --argument C --skeptical_acceptance 0.5
Checking skeptical acceptance of argument C with threshold 0.5 under the following semantics: JntCmp
C is not skeptically accepted.
Counterexample:
Support:
P(-A,-B,-C) = 1
The output tells us that `C` is not skeptically accepted under the given constraints and additionally provides a distribution which is a counterexample, in this case a joint-complete distribution with `P(C) = 0`.
### Generate labelings ### Generate labelings
`-OL`, `--one_labeling` For tasks involving labelings, a labeling scheme needs to be specified.
A list of all available labeling schemes is printed with the `--list_labeling_schemes` (or `-ll`) flag.
Note that the `--documentation` (or `-d`) flag also works with labeling schemes and displays a short description:
$ cpraa --list_labeling_schemes
Available labeling schemes: Cautious, Threshold, Firm, ClassicalOld, ThresholdClassicalOld, Classical, ThresholdClassical, Optimistic, Pessimistic
$ cpraa --documentation Cautious
Labeling scheme 'Cautious':
Arguments with probability 1 are labeled 'in', those with probability 0 are labeled 'out' and all others are
labeled 'undec'.
Some labeling schemes require one or more thresholds which can be specified following the `--labeling_threshold` (or `-lt`) flag.
Given all that, either one labeling or all labelings can be computed with `--one_labeling` (`-OL`) and `--all_labelings` (`-AL`).
`-AL`, `--all_labelings` **Example:** Compute all min-complete labelings under the `Firm` labeling scheme:
(TODO) $ cpraa -f AFs/example.tgf --semantics MinCmp --labeling_scheme firm --all_labelings
Computing all firm labelings satisfying the following semantics: MinCmp
Number of labelings: 6
{}{}{A,B,C}
{}{A,B,C}{}
{}{A,C}{B}
{}{B}{A,C}
{A,C}{B}{}
{B}{A,C}{}
Labelings are printed in set notation in the order `{in}{out}{undec}`.
That is, the labeling `{B}{A,C}{}` means argument `B` is labeled _in_, `A` and `C` are both _out_, and no argument is labeled as _undecided_.
## Further options ## Further options
### Additional constraints as SMT file
`-smt`, `--smt_file` `-smt`, `--smt_file`
In the input format section, we saw that additional constraints on the marginal probabilities of arguments can be specified directly in the input file.
More involved constraints can be added via an extra file in [SMT-LIB](https://smtlib.cs.uiowa.edu/) format.
Note that this functionality is currently only available for tasks that do not require linear constraints.
**Example:** The file `example.smt` contains the following additional constraints for the AF `example.tgf`:
; P(A) = 2 ∗ P(C)
(declare-fun p_A () Real)
(declare-fun p_C () Real)
(assert (= p_A (* 2 p_C)))
; P(A ∨ C | -B) ≥ 0.8
; P((A ∨ C) ∧ -B) ≥ 0.8 ∗ P(-B)
; P(A ∧ -B) + P(C ∧ -B) - P(A ∧ C ∧ -B) ≥ 0.8 ∗ P(-B)
(declare-fun p_A_nB () Real)
(declare-fun p_nB_C () Real)
(declare-fun p_A_nB_C () Real)
(declare-fun p_nB () Real)
(assert (>= (- (+ p_A_nB p_nB_C) p_A_nB_C) (* 0.8 p_nB)))
To express the constraint `P(A) = 2 ∗ P(C)`, i.e., that `A` is twice as likely as `C`, we need two variables `p_A` and `p_C` which refer to the marginal probabilities of `A` and `C`.
The constraint is then given in assert statement using prefix notation: `(assert (= p_A (* 2 p_C)))`.
For the constraint `P(A ∨ C | -B) ≥ 0.8`, i.e., the conditional probability of `A` or `C` holding given that `B` does not hold is at least `0.8`, we need to rewrite the constraint such that only statements about the probability of conjunctions remain: `P(A ∧ -B) + P(C ∧ -B) - P(A ∧ C ∧ -B) ≥ 0.8 ∗ P(-B)`.
Thus, variables need to be introduced for `P(A ∧ -B)`, `P(C ∧ -B)`, `P(A ∧ C ∧ -B)` and `P(-B)`: `p_A_nB`, `p_nB_C`, `p_A_nB_C` and `p_nB`.
Note how negation is represented by a leading `n` and that the argument names `A`, `B` and `C` always appear in lexicographic order.
This is required for correct parsing of the constraints.
Looking for one joint-complete distribution which satisfies the above constraints yields the following:
$ cpraa --file AFs/example.tgf --smt_file AFs/example.smt --semantics JntCmp --one_distribution
SMT constraint: ((p_A = (2.0 * p_C)) & ((4/5 * p_nB) <= ((p_A_nB + p_nB_C) - p_A_nB_C)))
Computing one distribution satisfying the following semantics: JntCmp
Support:
P(-A, B,-C) = 1
### Specify which solver to use
`-b`, `--backend_solver` `-b`, `--backend_solver`
By default, CPrAA automatically picks a fitting solver to use as backend for each task.
With this flag, usage of a specific solver can be enforced.
Options are all SMT solvers available via [pySMT](https://github.com/pysmt/pysmt) (`z3`, `msat`, `cvc4`, `yices`, `btor`, `picosat`, `bdd`), linear solvers via [CVXOPT](https://github.com/cvxopt/cvxopt) (`cvxopt`, `glpk`, `mosek`), and a direct integration of Z3 (`z3-legacy`).
While Z3 and CVXOPT are dependencies of CPrAA and thus always available, most of the other solvers need to be installed separately.
More information on how to install the listed SMT solvers is given in the [documentation](https://pysmt.readthedocs.io/en/latest/getting_started.html) of pySMT.
### Time the execution
`-t`, `--time` `-t`, `--time`
With this flag, some timings are printed, including the overall runtime and how long it took to generate all constraints.
Note that some given timings may include other timings (e.g., the timing for the task may include the timing for the constraint generation), so the sum of given partial timings can exceed the overall runtime.
$ cpraa --file AFs/example.tgf --semantics MinCmp --one_distribution --time
Computing one distribution satisfying the following semantics: MinCmp
solver instance setup took 0.002 seconds
Generating constraints for all semantics took 0.002 seconds
Support:
P( A,-B, C) = 1
Computing one distribution took 0.020 seconds
Overall runtime: 0.025 seconds
<!--
### Output format options for distributions
`-o`, `--distribution_output_format` `-o`, `--distribution_output_format`
`-p`, `--output_precision` `-p`, `--output_precision`
-->
### Display the constraints of the semantics
`-dc`, `--display_constraints` `-dc`, `--display_constraints`
With this flag, the constraints generated for the give AF under the given semantics are displayed.
Very long constraints are truncated.
Note that for complemented semantics, the constraints are displayed without the subsequent conjunction and negation.
If a semantics generates one constraint for each attack or each argument in the AF, then the attack's or argument's name is given before the constraint.
**Example:**
$ cpraa --file AFs/example.tgf --semantics MinCmp --one_distribution --display_constraints
Computing one distribution satisfying the following semantics: MinCmp
CF: A->B: (p_A_B = 0.0)
CF: B->C: (p_B_C = 0.0)
CF: B->A: (p_A_B = 0.0)
MinAdm: A: (p_A <= (1.0 - p_nA))
MinAdm: B: (p_B <= (1.0 - p_nB))
MinAdm: C: (p_C <= (1.0 - p_nA))
MinCmp: A: ((p_A_nB_nC + p_A_B_nC + p_A_nB_C + p_A_B_C) <= p_A)
MinCmp: B: ((p_nA_B_nC + p_nA_B_C + p_A_B_nC + p_A_B_C) <= p_B)
MinCmp: C: ((p_A_nB_nC + p_A_B_nC + p_A_nB_C + p_A_B_C) <= p_C)
Support:
P( A,-B, C) = 1
(TODO) Min-completeness requires min-admissibility, which in turn enforces conflict-freeness.
\ No newline at end of file Thus, we first see the constraints generated by CF for each attack, followed by the MinAdm constraints and MinCmp constraints for each argument.
\ No newline at end of file
...@@ -4,7 +4,7 @@ from typing import List ...@@ -4,7 +4,7 @@ from typing import List
import af_parser import af_parser
import labeling_scheme as lab import labeling_scheme as lab
from labeling import Labeling from labeling import Labeling
from linear_solver import LinearSolver, LinearConstraintError from linear_solver import LinearSolver
from DPGM import DPGM from DPGM import DPGM
import semantics as sem import semantics as sem
import tasks import tasks
...@@ -14,14 +14,15 @@ from timer import Timer ...@@ -14,14 +14,15 @@ from timer import Timer
# TODO: # TODO:
# - produce log files # - produce log files
# - task to get distribution unequal to a given other distribution? # - set verbosity level, or add silent mode
# - re-add assume-independence flag # - re-add assume-independence flag
#
# - task to get distribution unequal to a given other distribution?#
# - Flag for extensions # - Flag for extensions
# - flag to generate unsat core; this needs named assertions, see assert_and_track() in z3.py # - flag to generate unsat core; this needs named assertions, see assert_and_track() in z3.py
# - credulous and skeptical acceptance wrt. a labeling scheme # - credulous and skeptical acceptance wrt. a labeling scheme
__version__ = "0.7.0" __version__ = "0.7.1"
# Solvers # Solvers
Z3_LEGACY = "z3-legacy" Z3_LEGACY = "z3-legacy"
......
...@@ -195,15 +195,15 @@ def get_all_satisfying_labelings(si: SolverInstance, lab: LabelingScheme, semant ...@@ -195,15 +195,15 @@ def get_all_satisfying_labelings(si: SolverInstance, lab: LabelingScheme, semant
labelings.add(labeling) labelings.add(labeling)
candidate_constraints = next_candidate_constraints candidate_constraints = next_candidate_constraints
# How many constraints do we have for each node? Usually as many as there are labelings, though for some labeling # # How many constraints do we have for each node? Usually as many as there are labelings, though for some labeling
# schemes there are fewer # # schemes there are fewer
branching = len(lab.get_constraints(list(si.af.get_nodes())[0], si)) # branching = len(lab.get_constraints(list(si.af.get_nodes())[0], si))
# number of nodes in a perfect k-ary tree of depth n = number of nodes and k = branching, # # number of nodes in a perfect k-ary tree of depth n = number of nodes and k = branching,
# i.e., wc = (k**(n+1) - 1) // (k-1) # # i.e., wc = (k**(n+1) - 1) // (k-1)
worst_case_checks = (branching**(len(si.af.get_nodes()) + 1) - 1) // (branching - 1) # worst_case_checks = (branching**(len(si.af.get_nodes()) + 1) - 1) // (branching - 1)
#
print("Finished. Performed {} checks (worst case: {}) and found {} labelings.".format( # print("Finished. Performed {} checks (worst case: {}) and found {} labelings.".format(
num_of_checks, worst_case_checks, len(labelings))) # num_of_checks, worst_case_checks, len(labelings)))
return labelings return labelings
...@@ -267,15 +267,15 @@ def get_all_satisfying_labelings_z3(z3i: Z3Instance, lab: LabelingScheme, semant ...@@ -267,15 +267,15 @@ def get_all_satisfying_labelings_z3(z3i: Z3Instance, lab: LabelingScheme, semant
z3i.solver.pop() # go back to the backtracking point z3i.solver.pop() # go back to the backtracking point
candidate_constraints = next_candidate_constraints candidate_constraints = next_candidate_constraints
# How many constraints do we have for each node? Usually as many as there are labelings, though for some labeling # # How many constraints do we have for each node? Usually as many as there are labelings, though for some labeling
# schemes there are fewer # # schemes there are fewer
branching = len(lab.get_constraints_z3(list(z3i.af.get_nodes())[0], z3i)) # branching = len(lab.get_constraints_z3(list(z3i.af.get_nodes())[0], z3i))
# number of nodes in a perfect k-ary tree of depth n = number of nodes and k = branching, # # number of nodes in a perfect k-ary tree of depth n = number of nodes and k = branching,
# i.e., wc = (k**(n+1) - 1) // (k-1) # # i.e., wc = (k**(n+1) - 1) // (k-1)
worst_case_checks = (branching**(len(z3i.af.get_nodes()) + 1) - 1) // (branching - 1) # worst_case_checks = (branching**(len(z3i.af.get_nodes()) + 1) - 1) // (branching - 1)
#
print("Finished. Performed {} checks (worst case: {}) and found {} labelings.".format( # print("Finished. Performed {} checks (worst case: {}) and found {} labelings.".format(
num_of_checks, worst_case_checks, len(labelings))) # num_of_checks, worst_case_checks, len(labelings)))
return labelings return labelings
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment