通过子句组求解器 API 增量计算 QBF 的最小不可满足核
计算机科学中的逻辑
2015-09-21 v4
摘要
我们考虑 QBF 的最小不可满足核（MUCs）的增量计算。为此，我们为增量 QBF 求解器 DepQBF 配备了一个新颖的 API，以支持基于子句组的增量求解。子句组是一组子句，可增量地添加至先前已求解的 QBF 或从其中移除。我们对这一新颖 API 的实现与基于选择变量和假设的增量 SAT 求解相关。然而，该 API 向用户完全隐藏了选择变量和假设，从而便于在其他工具中集成 DepQBF。我们给出了实现细节，并首次报道了使用 DepQBF 的新颖子句组 API 计算 QBF 的 MUCs 的相关实验。
引用
@article{arxiv.1502.02484,
title = {Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API},
author = {Florian Lonsing and Uwe Egly},
journal= {arXiv preprint arXiv:1502.02484},
year = {2015}
}
备注
(fixed typo), camera-ready version, 6-page tool paper, to appear in proceedings of SAT 2015, LNCS, Springer