中文

增量式 QBF 求解

计算机科学中的逻辑 2014-09-05 v3

摘要

我们考虑增量式求解一系列量化布尔公式(QBF)的问题。增量求解旨在利用从序列中前一个公式学到的信息来求解后续公式。基于对该问题及相关挑战的总体概述,我们提出了一种与应用无关的增量式 QBF 求解方法,因此适用于任意问题的 QBF 编码。我们在基于增量搜索的 QBF 求解器 DepQBF 中实现了该方法,并报告了实现细节。实验结果展示了增量求解在基于 QBF 的工作流中的潜在优势。

关键词

引用

@article{arxiv.1402.2410,
  title  = {Incremental QBF Solving},
  author = {Florian Lonsing and Uwe Egly},
  journal= {arXiv preprint arXiv:1402.2410},
  year   = {2014}
}

备注

revision (camera-ready, to appear in the proceedings of CP 2014, LNCS, Springer)