论证性质的结构感知编码用于 Clique-width

图的结构度量（如 treewidth）是计算复杂性中的重要工具，结果导致在参数受控时高效算法。甚至已知现代 SAT 求解器在小 treewidth 的实例上高效工作。鉴于这些求解器广泛应用，研究兴趣转向对求解的紧凑编码以及编码限制的理解。更一般的是图参数 clique-width，这与 treewidth 不同，适用于稠密图。虽然可获得 clique-width 的算法，但关于编码的了解仍有限。我们致力于理解 clique-width 编码能力的探索，通过考虑抽象论证，这是一种处理冲突论证的稳健框架。它基于有向图并询问计算上具有挑战性的性质，使其成为研究计算性质的自然候选。我们设计从论证问题到 (Q)SAT 的新型归约。我们的归约线性保持 clique-width，结果为有向分解导向（DDG）归约。我们为所有论证语义（包括计数）建立了新结果。值得注意的是，我们的 DDG 归约造成的开销在合理假设下无法显著改进。