Beyersdorff Olaf, Blinkhorn Joshua, Mahajan Meena
Institut für Informatik, Friedrich-Schiller-Universität Jena, Jena, Germany.
The Institute of Mathematical Sciences, HBNI, Chennai, India.
J Autom Reason. 2021;65(1):125-154. doi: 10.1007/s10817-020-09560-1. Epub 2020 May 22.
Strategy extraction is of great importance for quantified Boolean formulas (QBF), both in solving and proof complexity. So far in the QBF literature, strategy extraction has been algorithmically performed proofs. Here we devise the first QBF system where (partial) strategies are built the proof and are piecewise constructed by simple operations along with the derivation. This has several advantages: (1) lines of our calculus have a clear semantic meaning as they are accompanied by semantic objects; (2) partial strategies are represented succinctly (in contrast to some previous approaches); (3) our calculus has strategy extraction by design; and (4) the partial strategies allow new sound inference steps which are disallowed in previous central QBF calculi such as Q-Resolution and long-distance Q-Resolution. The last item (4) allows us to show an exponential separation between our new system and the previously studied reductionless long-distance resolution calculus. Our approach also naturally lifts to dependency QBFs (DQBF), where it yields the first sound and complete CDCL-style calculus for DQBF, thus opening future avenues into CDCL-based DQBF solving.
策略提取对于量化布尔公式（QBF）在求解和证明复杂度方面都非常重要。到目前为止，在QBF文献中，策略提取一直是通过算法来执行证明的。在此，我们设计了首个QBF系统，其中（部分）策略是在证明过程中构建的，并且通过简单操作与推导一起逐段构建。这具有几个优点：（1）我们演算中的行具有明确的语义含义，因为它们伴随着语义对象；（2）部分策略的表示简洁（与一些先前的方法形成对比）；（3）我们的演算在设计上具有策略提取功能；（4）部分策略允许进行新的合理推理步骤，而这些步骤在诸如Q-归结和远程Q-归结等先前的核心QBF演算中是不允许的。最后一项（4）使我们能够展示新系统与先前研究的无归约远程归结演算之间的指数级分离。我们的方法自然地也适用于依赖QBF（DQBF），在此它产生了首个用于DQBF的合理且完备的冲突驱动子句学习（CDCL）风格演算，从而为基于CDCL的DQBF求解开辟了未来的道路。
