k-Solutions: A Solver for the Dynamic Track of ICCMA 2023

In this system description we present k-Solutions, a solver submission for the dynamic track of the fifth International Competition on Computational Models of Argumentation (ICCMA). Our approach is to compute k-many witnesses to problems posed in the dynamic track using the state-of-the-art SAT solver Z3. For instance, for credulous acceptance under admissibility, we compute (up to) k-many admissible sets containing a queried argument. After subsequent changes, we only re-compute if witnesses are not preserved under the modifications. Our solver can answer credulous acceptance under complete and stable semantics, and skeptical acceptance under stable semantics.