Neue Encodings für Argumentationsgraphen: Clique‑Width bleibt unverändert

In der Welt der Graphentheorie sind strukturelle Messgrößen wie der Treewidth zentrale Werkzeuge, die effiziente Algorithmen ermöglichen, wenn man sie als Parameter nutzt. Besonders bekannt ist, dass moderne SAT‑Solver bei Instanzen mit kleinem Treewidth sehr schnell arbeiten. Da diese Solver weit verbreitet sind, besteht ein starkes Interesse an kompakten Encodings in (Q)SAT, um sowohl Lösungen zu finden als auch die Grenzen solcher Encodings zu verstehen.

Ein noch weniger erforschtes Maß ist der Clique‑Width, der auch bei dichten Graphen klein sein kann. Obwohl Algorithmen für Clique‑Width existieren, ist wenig darüber bekannt, wie gut graphbasierte Probleme in (Q)SAT enkodiert werden können. Die vorliegende Arbeit startet die Untersuchung dieser Frage, indem sie das robuste Framework der abstrakten Argumentation heranzieht.

Abstrakte Argumentation basiert auf gerichteten Graphen und verlangt nach der Berechnung anspruchsvoller Eigenschaften – ein idealer Kandidat, um die Komplexität von Encodings zu analysieren. Die Autoren entwickeln neue Reduktionen von Argumentationsproblemen auf (Q)SAT, die den Clique‑Width linear erhalten. Diese sogenannten Directed Decomposition‑Guided (DDG) Reduktionen gelten für sämtliche Argumentationssemantiken, einschließlich der Zählung von Lösungen.

Ein bemerkenswertes Ergebnis ist, dass die durch DDG‑Reduktionen entstehende Overhead nicht signifikant reduziert werden kann, sofern vernünftige Annahmen gelten. Damit liefert die Studie nicht nur neue, effiziente Encodings, sondern legt auch fundamentale Grenzen für die Optimierung solcher Verfahren nahe.