HordeQBF：一种模块化的大规模并行 QBF 求解器
计算机科学中的逻辑
2016-06-15 v1 人工智能
摘要
最近开发的大规模并行可满足性（SAT）求解器 HordeSAT 以模块化方式设计，以允许在其核心中集成任何基于 CDCL 的顺序 SAT 求解器。我们将基于 QCDCL 的量化布尔公式（QBF）求解器 DepQBF 集成到 HordeSAT 中，得到大规模并行 QBF 求解器——HordeQBF。本文中我们描述了该集成的细节，并报告了 HordeQBF 性能实验评估的结果。HordeQBF 在 2014 年 QBF Gallery 的困难应用实例上实现了超线性的平均和中位数加速。
引用
@article{arxiv.1604.03793,
title = {HordeQBF: A Modular and Massively Parallel QBF Solver},
author = {Tomas Balyo and Florian Lonsing},
journal= {arXiv preprint arXiv:1604.03793},
year = {2016}
}
备注
camera-ready version, 6-page tool paper, to appear in the proceedings of SAT 2016, LNCS, Springer