← 研踪 PaperTrailarXiv:2611.10633 · v1
An Improved Algorithm for Quantified Boolean Formulas
首次提交 2026-11-07 18:21
版本更新 2026-11-07 18:21
雷达观测 2026-11-10 11:14
摘要
Quantified Boolean formula (QBF), the quantified version of Boolean satisfiability (SAT), is a fundamental problem in constraint solving. Due to the $\mathsf{PSPACE}$-complete nature of QBF, designing theoretically efficient QBF algorithms is much harder and receives less attention in academia. In this work, we present a new algorithm based on memoized search, which solves QBF with $n$ variables and $m$ clauses in $1.685^m\cdot\text{poly}(n)$ time and space. This is the first improvement over the $1.709^m\cdot\text{poly}(n)$ bound by Williams in over 20 years. Our technique is based on the minimum vertex cover of the conflict graphs, which was proposed to study the parameterized complexity of SAT. We extend this idea to QBF and further show that QBF is slicewise polynomial-time solvable using this parameter.
观测到的版本
相邻记录可能跳过中间版本；首次发现 v2 及以上也会标为版本更新。
v1 · 2026-11-07 18:21 · 最新观测版本
An Improved Algorithm for Quantified Boolean Formulas
Quantified Boolean formula (QBF), the quantified version of Boolean satisfiability (SAT), is a fundamental problem in constraint solving. Due to the $\mathsf{PSPACE}$-complete nature of QBF, designing theoretically efficient QBF algorithms is much harder and receives less attention in academia. In this work, we present a new algorithm based on memoized search, which solves QBF with $n$ variables and $m$ clauses in $1.685^m\cdot\text{poly}(n)$ time and space. This is the first improvement over the $1.709^m\cdot\text{poly}(n)$ bound by Williams in over 20 years. Our technique is based on the minimum vertex cover of the conflict graphs, which was proposed to study the parameterized complexity of SAT. We extend this idea to QBF and further show that QBF is slicewise polynomial-time solvable using this parameter.
查看此版本解读 →查看此版本原文 ↗