保持树宽的普通 ASP 到 SAT 的归约——普通 ASP 终究比 SAT 更难吗？

答案集编程 (Answer Set Programming, ASP) 是一种用于知识表示与推理问题建模和求解的范式。有大量结果致力于研究 ASP（的片段）的困难性。迄今为止，这些研究得出了计算复杂性方面的刻画，以及以二分风格结果、翻译到其他形式化如命题可满足性 (SAT) 时的下界、甚至详细的参数化复杂性图景等形式呈现的细粒度洞察。参数化复杂性中源自图论的一个通用参数是所谓的树宽，它在某种意义上刻画了程序的结构稠密性。近来，与 SAT 相关的基于树宽的求解器数量有所增加。虽然存在从（普通）ASP 到 SAT 的翻译，但尚无保持树宽或至少追踪树宽增长的归约已知。本文中，我们提出一种从普通 ASP 到 SAT 的、感知树宽的新归约，并保证树宽的轻微增加确实足够。进一步，我们给出一个新结果，确立当考虑树宽时，即便普通 ASP 的片段也已比 SAT 略难（在计算复杂性的合理假设下）。这也确认了我们的归约或许无法被显著改进，且树宽的轻微增加是不可避免的。最后，我们给出了从普通 ASP 到 SAT 的新归约的实证研究，其中我们比较通过已知分解启发式获得的树宽上界。总体而言，我们的归约在这些启发式下比现有翻译表现更好。