Counterexample-Guided Abstraction Refinement for Assumption-based Argumentation

Assumption-Based Argumentation (ABA) is a prominent formalism for structured argumentation, widely applied in domains such as healthcare, law, and robotics.

Despite its inherent computational complexity, ABA has seen the development of effective techniques that successfully address key tasks, including evaluating the acceptability of literals and computing framework extensions.

These approaches typically involve translating the initial ABA framework into an intermediate formalism, such as an Answer Set Program or an Abstract Argumentation Framework, which is then encoded into a Boolean satisfiability (SAT) problem.

However, this translation can lead to large and complex intermediate representations, posing challenges for state-of-the-art SAT solvers.

In this work, we propose a Counterexample-Guided Abstraction Refinement (CEGAR) approach that bypasses the initial translation step, at the cost of incrementally discovering certain ABA constraints that are not explicitly captured in the initial SAT encoding.

We analyze the performance of our method and demonstrate that it outperforms state-of-the-art approaches on specific problem classes, while remaining competitive with the best existing solvers more broadly.