LabSAT is a solver for reasoning tasks in abstract argumentation frameworks1. It utilizes the labelling approach by Caminada as a satisfiability problem (SAT)2.
As participant of the ICCMA'153 LabSAT solves the following computational tasks:
- Given an abstract argumentation framework, determine some extension
- Given an abstract argumentation framework, determine all extensions
- Given an abstract argumentation framework and some argument, decide whether the given argument is credulously inferred
- Given an abstract argumentation framework and some argument, decide whether the given argument is skeptically inferred
The above computational tasks are solved with respect to the following standard semantics:
- Complete Semantics
- Preferred Semantics
- Grounded Semantics
- Stable Semantics
The LabSAT-Solver Paper contains a detailed description of the technique used.
At least java 7, maven, gcc and make are required. The environment variable $JAVA_HOME has to be set accordingly.
chmod 755 build
./build
solver --formats
Prints the supported formats of the solver.
solver --problems
Prints the supported computational problems.
solver -p <problem> -f <file> -fo <fileformat> [-a <argument of search>]
Starts the computation.
1 Dung, P. M., On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games, in: Artificial Intelligence, vol. 77, pp. 321–357 (1995)
2 Cerutti, F., Dunne P., Giacomin, M., Vallati, M.: A SAT-based Approach for Computing Extensions in Abstract Argumentation, in: Black, E., Modgil, S., Oren, N.(eds.), Theory and Applications of Formal Argumentation – Second International Workshop (TAFA 2013), Lecture Notes in Computer Science, vol. 8306, pp. 176–193. Springer, Berlin (2014)
3 http://argumentationcompetition.org/2015