增量式 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)