README.md 16.9 KB
Newer Older
Nikolai Käfer's avatar
Nikolai Käfer committed
1
2
3
4
5
6
7
8
# CPrAA - A Checker for Probabilistic Abstract Argumentation

[![PyPI](https://img.shields.io/pypi/v/cpraa "View CPrAA on PyPI")](https://pypi.org/project/cpraa/)

CPrAA is a Python tool and package for various tasks in probabilistic abstract argumentation:
 * find distributions satisfying numerous probabilistic argumentation semantics
 * check for credulous or skeptical acceptance of arguments
 * maximize or minimize the marginal probability of certain arguments
Nikolai Käfer's avatar
Nikolai Käfer committed
9
 * generate labelings according to different labeling schemes
Nikolai Käfer's avatar
Nikolai Käfer committed
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38


## Installation

CPrAA is available on [PyPI](https://pypi.org/project/cpraa/) and can be installed with `pip`:

    pip install cpraa

Note that Python 3.7 or higher is required.


## Basic usage

For usage as a command-line tool, locate your installation of `cpraa` with `pip show cpraa`:

    $ pip show cpraa
    Name: cpraa
    Version: 0.6.1
    [...]
    Location: /path/to/installation

Change to the directory `/path/to/installation/cpraa` and run `python main.py --help` to display the built-in help message of CPrAA.
For the remainder of this readme we assume a shortcut `cpraa` is created which resolves to `python main.py` in this directory.

Basic usage usually requires at least three flags:
   * `--file` (or `-f`) followed by a `.tgf` file specifying the argumentation framework
   * `--semantics` (or `-s`) followed by the names of one or more semantics
   * the task to perform, e.g. `--one_distribution` to compute one distribution which satisfies the constraints of all specified semantics

Nikolai Käfer's avatar
Nikolai Käfer committed
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
**Example:**

    $ cpraa --file AFs/example.tgf --semantics MinCmp --one_distribution
    Computing one distribution satisfying the following semantics: MinCmp
    Support:
    P( A,-B, C) = 1

The result shows a distribution in _support format_, that is, only the assignments with non-zero probabilities are shown.
In this case, `P( A,-B, C) = 1` means that the assignment where `A` and `C` hold while `B` does not hold has a probability of one under this distribution.
To get the full distribution, the flag `--distribution_output_format` (or just `-o` for short) can be used with parameter `F`.
Likewise, the parameter `M` can be passed with the same flag to display the marginal probabilities of all arguments, and it is possible to pass multiple format options at once:

    $ cpraa --file AFs/example.tgf --semantics MinCmp --one_distribution --distribution_output_format FM
    Computing one distribution satisfying the following semantics: MinCmp
    P(-A,-B,-C) = 0
    P(-A,-B, C) = 0
    P(-A, B,-C) = 0
    P(-A, B, C) = 0
    P( A,-B,-C) = 0
    P( A,-B, C) = 1
    P( A, B,-C) = 0
    P( A, B, C) = 0
    P(A) = 1
    P(B) = 0
    P(C) = 1
Nikolai Käfer's avatar
Nikolai Käfer committed
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101


## Input format

Argumentation frameworks (AFs) are provided in trivial graph format (`.tgf`) with some optional extensions.
A simple AF with three nodes (`A`, `B`, `C`) and three edges (`A -> B`, `B -> A`, `B -> C`) is specified as follows:

    A
    B
    C
    #
    A B
    B A
    B C

That is, we first have a declaration of nodes with one node ID per line, then a separator `#`, and finally the declaration of attacks, again with one attack per line.
Empty lines are ignored, and `;` introduces a line comment.

Nodes can optionally be annotated with a name. This can be handy to keep IDs short even if the name is long. 
Further, nodes can be annotated with a numeric value (e.g. `0.75` or `1`) or a value interval (e.g. `0.1:0.3`).
These values or intervals can be used by semantics to impose further constraints. 
Most prominently, the `AF` semantics enforces a node's marginal probability to equal the given value or fall within the specified interval if either is given.

The general format for a node declaration is

> `<node_id>` [ `<node_name>` ] [ `<node_value>` | `<node_value_min>` `:` `<node_value_max>` ] [ `;` `<comment>`]

where `<node_id>` is an alphanumeric string, `<node_name>` is alphanumeric but does not start with a digit, and `<node_value>`, `<node_value_min>`, and `<node_value_max>` are either integers or floats.

Edge declarations consist of two node IDs and can likewise be annotated with a name and a value or an interval:

> `<from_node_id>` `<to_node_id>` [ `<edge_name>` ] [ `<edge_value>` | `<edge_value_min>` `:` `<edge_value_max>` ] [ `;` `<comment>`]

The folder `AFs` contains a number of example argumentation frameworks in `.tgf` format.


## Semantics

Nikolai Käfer's avatar
Nikolai Käfer committed
102
103
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`).
Nikolai Käfer's avatar
Nikolai Käfer committed
104

Nikolai Käfer's avatar
Nikolai Käfer committed
105
A list of all available semantics can be viewed with `--list_semantics` (or `-ls`):
Nikolai Käfer's avatar
Nikolai Käfer committed
106
107

    $ cpraa --list_semantics
Nikolai Käfer's avatar
Nikolai Käfer committed
108
    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
Nikolai Käfer's avatar
Nikolai Käfer committed
109

Nikolai Käfer's avatar
Nikolai Käfer committed
110
Tip: With `--documentation` (or `-d`) followed by the names of one or more semantics a short description of most semantics is available:
Nikolai Käfer's avatar
Nikolai Käfer committed
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176

    $ cpraa --documentation Fou MinAdm
    Semantics 'Fou':
        Foundedness semantics: Initial nodes must hold with probability 1.
    
    Semantics 'MinAdm':
        Min-admissibility semantics: CF and for every argument C, P(C) <= min_{B in Pre(C)} P(OR Pre(B)) holds.
        Equivalently, for all B in Pre(C) with Pre(B) = {A1, ..., An}, it holds P(C) <= 1 - P(nA1, ..., nAn).


## Tasks

Before taking a closer look at the tasks offered by CPrAA, it is worth noting that not all tasks are available for all semantics.
This is because, e.g., the optimization tasks are only feasible when facing _linear_ constraints.
However, for some semantics the imposed constraints are polynomial (rendering a formulation in terms of linear constraints impossible), or linear constraints are not yet implemented.
Notably, and perhaps most inconveniently, complement semantics are not available for tasks requiring linear constraints. 


### Check satisfiability 
`-OD`, `--one_distribution`

Basic task to check if the constraints imposed by all selected semantics are satisfiable.
If so, a satisfying distribution is returned as witness. 
Note that such a distribution in many cases is not the unique solution but only one representative from an infinite solution space. 

**Example:** Look for a distribution on the example AF that is min-complete (`MinCmp`) but not justifiable (`Jus`):

    $ cpraa -f AFs/example.tgf --semantics MinCmp --complement_semantics Jus --one_distribution
    Computing one distribution satisfying the following semantics: MinCmp, co-Jus
    Support:
    P(-A,-B, C) = 0.5
    P( A,-B,-C) = 0.5


### Enumerate vertices of convex solution space 
`-CD`, `--corner_distributions`

This task requires linear constraints, as otherwise it is not guaranteed that the solution space is convex.
The distributions (viewed as vectors in n-dimensional space) located at the corners of a convex solution space have the nice property that all solutions can be stated as a convex combination of them.
In case this task yields only a single distribution, the solution is unique.

**Example:** Find the corner distributions for element-wise completeness (`ElmCmp`) in the example AF:

    $ cpraa -f AFs/example.tgf --semantics ElmCmp --corner_distributions
    Computing the corner distributions for the following semantics: ElmCmp
    
    Result 1 of 3:
    Support:
    P(-A,-B,-C) = 1
    
    Result 2 of 3:
    Support:
    P(-A, B,-C) = 1
    
    Result 3 of 3:
    Support:
    P( A,-B, C) = 1

As expected, the resulting distributions are the Dirac distributions of the assignments corresponding to all three complete assignments of the example AF. 


### Optimize marginal probabilities

`-MIN`, `--minimize_probability`, or `-MAX`, `--maximize_probability`

This task requires linear constraints and one or more arguments from the AF (passed with `--arguments` or `-a`).
Nikolai Käfer's avatar
Nikolai Käfer committed
177
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.
Nikolai Käfer's avatar
Nikolai Käfer committed
178

Nikolai Käfer's avatar
Nikolai Käfer committed
179
**Example:** Find a probabilistically complete distribution under which argument `B`'s marginal probability is maximal: 
Nikolai Käfer's avatar
Nikolai Käfer committed
180

Nikolai Käfer's avatar
Nikolai Käfer committed
181
    $ cpraa -f AFs/example.tgf --semantics PrCmp -a B -MAX
Nikolai Käfer's avatar
Nikolai Käfer committed
182
183
184
185
186
187
188
    Computing optimal distribution maximizing the probability of argument B while satisfying the following semantics: PrCmp
    Support:
    P(-A, B,-C) = 1


### Acceptance checking for arguments

Nikolai Käfer's avatar
Nikolai Käfer committed
189
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.
Nikolai Käfer's avatar
Nikolai Käfer committed
190

Nikolai Käfer's avatar
Nikolai Käfer committed
191
192
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.
Nikolai Käfer's avatar
Nikolai Käfer committed
193

Nikolai Käfer's avatar
Nikolai Käfer committed
194
195
196
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`.  
Nikolai Käfer's avatar
Nikolai Käfer committed
197

Nikolai Käfer's avatar
Nikolai Käfer committed
198
**Example:** Check if argument `C` is skeptically accepted with a threshold of `0.5` under joint-complete semantics: 
Nikolai Käfer's avatar
Nikolai Käfer committed
199

Nikolai Käfer's avatar
Nikolai Käfer committed
200
201
202
203
204
205
206
207
    $ 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`.
Nikolai Käfer's avatar
Nikolai Käfer committed
208
209
210
211


### Generate labelings

Nikolai Käfer's avatar
Nikolai Käfer committed
212
213
214
215
216
217
218
219
220
221
222
223
224
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`).
Nikolai Käfer's avatar
Nikolai Käfer committed
225

Nikolai Käfer's avatar
Nikolai Käfer committed
226
**Example:** Compute all min-complete labelings under the `Firm` labeling scheme: 
Nikolai Käfer's avatar
Nikolai Käfer committed
227

Nikolai Käfer's avatar
Nikolai Käfer committed
228
229
230
231
232
233
234
235
236
    $ 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}{}
Nikolai Käfer's avatar
Nikolai Käfer committed
237

Nikolai Käfer's avatar
Nikolai Käfer committed
238
239
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_.
Nikolai Käfer's avatar
Nikolai Käfer committed
240
241
242

## Further options

Nikolai Käfer's avatar
Nikolai Käfer committed
243
244
### Additional constraints as SMT file 

Nikolai Käfer's avatar
Nikolai Käfer committed
245
246
`-smt`, `--smt_file`

Nikolai Käfer's avatar
Nikolai Käfer committed
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
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

Nikolai Käfer's avatar
Nikolai Käfer committed
286
287
`-b`, `--backend_solver`

Nikolai Käfer's avatar
Nikolai Käfer committed
288
289
290
291
292
293
294
295
296
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

Nikolai Käfer's avatar
Nikolai Käfer committed
297
298
`-t`, `--time`

Nikolai Käfer's avatar
Nikolai Käfer committed
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
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

Nikolai Käfer's avatar
Nikolai Käfer committed
315
316
317
`-o`, `--distribution_output_format`

`-p`, `--output_precision`
Nikolai Käfer's avatar
Nikolai Käfer committed
318
319
320
-->

### Display the constraints of the semantics  
Nikolai Käfer's avatar
Nikolai Käfer committed
321
322
323

`-dc`, `--display_constraints`

Nikolai Käfer's avatar
Nikolai Käfer committed
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
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
Nikolai Käfer's avatar
Nikolai Käfer committed
345

Nikolai Käfer's avatar
Nikolai Käfer committed
346
347
Min-completeness requires min-admissibility, which in turn enforces conflict-freeness.
Thus, we first see the constraints generated by CF for each attack, followed by the MinAdm constraints and MinCmp constraints for each argument.