SAT-based Reasoner for Abstract Dialectical Frameworks
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.
k++ADF is called from the command line as follows.
USAGE: ./adfsolver <sem> [options]
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.
k++ADF is available in open source under the MIT license at Bitbucket. Benchmark instance ADFs used in  are included in the repository.
 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.