k++ADF

SAT-based Reasoner for Abstract Dialectical Frameworks

k++ADF is developed by the Constraint Reasoning and Optimization Group at Department of Computer Science, University of Helsinki, and implemented by Andreas Niskanen.

About

Abstract Dialectical Frameworks (ADFs) are a powerful generalization of Argumentation Frameworks (AFs), providing a knowledge representation formalism in which arbitrary relations between arguments can be expressed by equipping each argument with an acceptance condition, i.e., a propositional formula. This expressive power comes with a price: compared to AFs, the computational complexity of reasoning tasks in ADFs, such as argument acceptance, is one level higher on the polynomial hierarchy. k++ADF provides complexity-sensitive algorithms for credulous and skeptical acceptance in ADFs, along with enumeration of interpretations, by making use of ADF subclasses where the complexity drops down to the same level as reasoning in AFs. Specifically, it detects whether the input ADF is k-bipolar for a sufficiently low value of k. The algorithms are based on utilizing SAT solvers as concrete NP oracles. Currently k++ADF supports the conflict-free, naive, admissible, complete, preferred, and grounded semantics.

Usage

k++ADF is called from the command line as follows.

USAGE: ./adfsolver <sem> [options] 

COMMAND LINE ARGUMENTS:
<file>  : Input filename for ADF instance.
<sem>   : ADF semantics. <sem>={cf|nai|adm|com|prf|grd}

COMMAND LINE OPTIONS:
-a <arg>: Query argument for acceptance problems.
-c      : Credulous acceptance. Requires the usage of -a flag.
-s      : Skeptical acceptance. Requires the usage of -a flag.
-l      : Output link types (att and sup).
-f      : Do not use k-bipolar encodings.
-n      : Do not use shortcuts for skeptical acceptance.
-h      : Display this help message.
-v      : Display the version of the program.

Input format

An input ADF instance consists of arguments and their acceptance conditions, which are expressed as follows.

s(a).    ... a is an argument
ac(a,f). ... the acceptance condition of a is f,
             where f is a propositional formula
             consisting of argument symbols,
             c(v) for true, c(f) for false,
             neg(p), and(p,q), or(p,q), xor(p,q),
             imp(p,q), iff(p,q), where p and q
             are subformulae.

Downloads

System

k++ADF is available in open source under the MIT license at Bitbucket. Benchmark instance ADFs used in [1] are included in the repository.

References

[1] Novel Algorithms for Abstract Dialectical Frameworks based on Complexity Analysis of Subclasses and SAT Solving. Thomas Linsbichler, Marco Maratea, Andreas Niskanen, Johannes P. Wallner, Stefan Woltran. Proceedings of the 27th International Joint Conference on Artificial Intelligence and the 23rd European Conference on Artificial Intelligence (IJCAI-ECAI 2018). To appear.
[pdf]