Structure-Aware Encodings of Argumentation Properties for Clique-width
Yasir Mahmood, Markus Hecher, Johanna Groven, Johannes K. Fichte
TL;DR
This work develops a framework for structure-aware encodings of abstract argumentation into SAT/2QBF by preserving directed clique-width through directed decomposition-guided (DDG) reductions using $k$-expressions. It provides $dcw$-preserving encodings for all standard argumentation semantics (stable, admissible, complete, preferred, semi-stable, stage) and extends to credulous and skeptical reasoning, achieving tractable upper bounds (e.g., $2^{ ext{O}(k)}$ or $2^{2^{ ext{O}(k)}}$ runtimes depending on semantics) while preserving linear cw-width. The paper also establishes lower bounds under ETH, showing that these reductions cannot be significantly improved, and demonstrates the practicality of maintaining clique-width structure even in dense attack graphs via DDG encodings. Overall, the results bridge KRR formalisms and SAT/QBF solvers under clique-width considerations, enabling efficient solving and counting of extensions across semantics and offering a path to generalize to other KRR formalisms. The approach leverages $k$-expressions to propagate semantic constraints along the construction, coupling combinatorial structure with logic-based encodings for scalable reasoning.
Abstract
Structural measures of graphs, such as treewidth, are central tools in computational complexity resulting in efficient algorithms when exploiting the parameter. It is even known that modern SAT solvers work efficiently on instances of small treewidth. Since these solvers are widely applied, research interests in compact encodings into (Q)SAT for solving and to understand encoding limitations. Even more general is the graph parameter clique-width, which unlike treewidth can be small for dense graphs. Although algorithms are available for clique-width, little is known about encodings. We initiate the quest to understand encoding capabilities with clique-width by considering abstract argumentation, which is a robust framework for reasoning with conflicting arguments. It is based on directed graphs and asks for computationally challenging properties, making it a natural candidate to study computational properties. We design novel reductions from argumentation problems to (Q)SAT. Our reductions linearly preserve the clique-width, resulting in directed decomposition-guided (DDG) reductions. We establish novel results for all argumentation semantics, including counting. Notably, the overhead caused by our DDG reductions cannot be significantly improved under reasonable assumptions.