QBF 的双侧树宽：策略与归结的交汇点
数据结构与算法
2026-05-08 v1 计算复杂性
摘要
树宽是一个被广泛研究的分解参数，用于衡量图的树状程度。虽然已知命题可满足性问题 (SAT) 在以底层原始图的树宽为参数时是可处理的，但量化布尔公式 (QBF) 的求值即使在常数树宽的公式上也仍然是 PSPACE 完全的。直觉上，这是因为普通树宽没有考虑 QBF 的前缀：它既不区分存在变量和全称变量，也不考虑它们被量化的顺序。过去，人们设计了树宽的几个较弱变体以纳入前缀敏感信息。为了在这些概念下建立 QBF 的可处理性，先前的工作要么采用基于策略的技术，要么采用基于归结的技术，从而将 QBF 的参数化复杂度图景划分为两个强度不可比较的区域。我们建立了关于双侧树宽的固定参数可处理性，这是一种新颖且严格更强大的分解参数，它通过同时允许对策略进行分支和执行 Q-归结来结合了这两种对立的方法。与该方向先前的工作一样，我们的算法假设在输入中提供了一个合适的树分解。
引用
@article{arxiv.2605.06262,
title = {Bilateral Treewidth for QBF: Where Strategies and Resolution Meet},
author = {Robert Ganian and Marlene Gründel},
journal= {arXiv preprint arXiv:2605.06262},
year = {2026}
}