## k++ADF## SAT-based Reasoner for Abstract Dialectical Frameworksk++ADF is developed by the Constraint Reasoning and Optimization Group at Department of Computer Science, University of Helsinki, and implemented by Andreas Niskanen. ## AboutAbstract 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. ## Usagek++ADF is called from the command line as follows. USAGE: ./adfsolver <sem> [options] ## Input formatAn 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## Systemk++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] |