SAT-based Argumentation Systems

SAT(isfiability) solvers are capable of handling large boolean formulas. Here we present tools based on SAT-solvers for abstract argumentation. They are developed within the project "Abstract Dialectical Frameworks: Advanced Tools for Formal Argumentation".

News
About
Usage
Team
Download
Related Webpages
References

News

Webpage online

10.6.2013
The webpage is now online and offers several tools for solving reasoning tasks in abstract argumentation in version 0.1 for download.

About

In the area of propositional satisfiability (SAT), tremendous progress has been made in the last decade. Today's SAT technology not only covers the standard SAT problem, but also extensions thereof, such as computing a backbone (the literals which are true in all satisfying assignments) or minimal corrections sets (MCS), which are minimal subsets of clauses which if dropped leave an originally unsatisfiable formula satisfiable. The algorithms presented here depend on these extensions to SAT to solve important problems from the area of abstract argumentation.

Usage

Here we provide the usage of our tools for semi-stable, ideal and eager semantics.

Input file conventions

We borrow the input file format from the ASPARTIX system. The parser will recognize the following lines:

arg(a). Argument a.
att(a,b). Attack relation between the arguments a and b.

The order of the definitions does not matter but only one attack or argument may be specified in one line.

Semi-stable Semantics based on MCS-solver

Command line options for Semi-stable semantics

First of all, let us take a look on some common program calls:

Skeptical acceptance of argument "a" with semi-stable semantics:
```
./semi.sh filename skept a
```
Credulous acceptance of argument "1" with semi-stable semantics:
```
./semi.sh filename cred 1
```
Enumeration of all semi-stable extensions :
```
./semi.sh filename enum
```
Output all skeptically accepted arguments for semi-stable semantics :
```
./semi.sh filename allSkept
```

We provide the complete usage (which is subject to change in future versions):

Usage: 
./semi.sh file <cred | skept | allSkept | enum> [argument]
file                    the file to read the AF from
cred                    cred(ulous) reasoning, requires argument
skept                   skept(ical) reasoning, requires argument
enum                    enum(eration) of all semi-stable extensions
allSkept                output all skeptically accepted arguments
argument                the argument for the query

Eager Semantics based on MCS-solver

Command line options for Eager semantics

First of all, let us take a look on some common program calls:

Eager extension:
```
./eager.sh filename
```

We provide the complete usage (which is subject to change in future versions):

Usage: 
./eager.sh file 
file                    the file to read the AF from

Ideal Semantics based on Backbone-solver

Command line options for Ideal semantics

First of all, let us take a look on some common program calls:

Ideal extension:
```
./ideal.sh filename
```

We provide the complete usage (which is subject to change in future versions):

Usage: 
./ideal.sh file 
file                    the file to read the AF from

Example

Let us consider the following input file containing the definition of a argumentation framework:

arg(a).
arg(b).
arg(c).
arg(d).
arg(e).
arg(f).
arg(g).
att(a,b).
att(c,b).
att(c,d).
att(d,c).
att(d,e).
att(e,g).
att(f,e).
att(g,f).

With this input, the program semi.sh will output the semi-stable extension "{a,d,g}".

Team

People involved in the development of the SAT-based algorithms:

Download

Here we provide the newest version of our algorithms as well as some benchmark examples for download. To run the software, download clingo (3.0.4) from potassco and add it to the directory. Then run the .sh files.

Version 0.1

Linux binaries for Semi-stable/Eager semantics (zip/tar archive)
Linux binaries for Ideal semantics (zip/tar archive)

Examples

Examples (approx 12MB): collection of examples from the literature and benchmark examples

Related Webpages

CAMUS
MiniSat
ASPARTIX
Clasp
arglib.org Towards an argumentation benchmark library

References

2013
[1]	Advanced SAT Techniques for Abstract Argumentation Johannes P. Wallner, Georg Weissenbacher and Stefan Woltran. In João Leite, Tran Cao Son, Paolo Torroni, Leon van der Torre and Stefan Woltran, editors, Proceedings of the Fourteenth International Workshop on Computational Logic in Multi-Agent Systems, CLIMA XIV, pages 138-154, Corunna, Spain, September 2013

Top

Home / Kontakt / Webmaster / Offenlegung gemäß § 25 Mediengesetz: Inhaber der Website ist das Institut für Informationssysteme an der Technischen Universität Wien, 1040 Wien. Die TU Wien distanziert sich von den Inhalten aller extern gelinkten Seiten und übernimmt diesbezüglich keine Haftung. / Disclaimer.