增量 SAT 与 QBF 求解器的自动基准测试
计算机科学中的逻辑
2015-12-04 v2
摘要
在求解相关公式序列时，增量 SAT 与 QBF 求解潜在地带来改进。增量应用通常针对某些特定求解器定制，并将问题分解为增量求解器调用。这阻碍了不同求解器的独立比较，尤其在应用程序不可用时。作为补救，我们提出一种增量 SAT 与 QBF 求解器的自动基准测试方法。给定由应用程序增量生成的 (Q)DIMACS 格式公式集合，我们的方法自动将这些公式翻译为导入并由增量 SAT/QBF 求解器求解公式的指令。翻译结果是一个重放增量求解器调用的程序，从而允许独立于应用程序评估增量求解器。我们通过 SAT 与 QBF 求解器的不同硬件验证问题来阐释我们的方法。
引用
@article{arxiv.1506.08563,
title = {Automated Benchmarking of Incremental SAT and QBF Solvers},
author = {Uwe Egly and Florian Lonsing and Johannes Oetsch},
journal= {arXiv preprint arXiv:1506.08563},
year = {2015}
}
备注
camera-ready version (8 pages + 2 pages appendix), to appear in the proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), LNCS, Springer, 2015