提出基于团宽的论证编码方法，提升逻辑求解效率。
Structure-Aware Encodings of Argumentation Properties for Clique-width
- 设计线性保持团宽的论证问题到(Q)SAT的映射方法
- 实现所有论证语义的高效编码，支持计数计算
- 证明该方法在合理假设下无法显著优化，适合理论研究者
图的结构度量如树宽是计算复杂性中的核心工具，能在参数较小时带来高效算法。现代SAT求解器在小树宽实例上表现优异，因此研究紧凑的(Q)SAT编码以理解其局限性成为热点。更一般的是团宽，它可在稠密图中仍保持较小，但相关编码研究极少。本文首次探索团宽在编码中的能力，聚焦于抽象论证框架——一种处理冲突论证的稳健推理模型。该框架基于有向图，涉及计算挑战性性质，适合作为研究计算特性的理想对象。我们设计了新的从论证问题到(Q)SAT的归约方法，其线性保持团宽，形成有向分解引导的（DDG）归约。我们在所有论证语义下建立了新结果，包括计数问题。值得注意的是，在合理假设下，该归约带来的开销无法被显著降低。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。