DepQBF 6.0：超越传统 QCDCL 的基于搜索的 QBF 求解器
计算机科学中的逻辑
2017-07-27 v2
摘要
我们展示了基于 QCDCL 的量化布尔公式（QBF）求解器 DepQBF 的最新主要版本 6.0。QCDCL 是冲突驱动子句学习（CDCL）范式的扩展，该范式在目前最先进的命题可满足性（SAT）求解器中实现。Q-归结演算（QRES）是支撑 QCDCL 的 QBF 证明系统。QCDCL 求解器可以在求解过程中，作为副产品生成前束合取范式（PCNF）下 QBF 的 QRES 证明。与基于 QRES 的传统 QCDCL 相比，DepQBF 6.0 实现了基于 QRES 泛化的一种 QCDCL 变体。这种泛化源于一组额外的公理，并保持了原有的 Q-归结规则不变。QRES 的泛化使得 QCDCL 有可能生成比传统变体指数级更短的证明。我们概述了 DepQBF 中实现的功能，并报告了实验结果，这些结果证明了泛化 QRES 在 QCDCL 中的有效性。
引用
@article{arxiv.1702.08256,
title = {DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL},
author = {Florian Lonsing and Uwe Egly},
journal= {arXiv preprint arXiv:1702.08256},
year = {2017}
}
备注
12 pages + appendix; to appear in the proceedings of CADE-26, LNCS, Springer, 2017