QBFRelay, QRATPre+, and DepQBF: Incremental Preprocessing Meets Search-Based QBF Solving
QBFRelay, QRATPre+, and DepQBF: Incremental Preprocessing Meets Search-Based QBF Solving
复制标题
QBFRelay、QRATPre 和 DepQBF：增量预处理满足基于搜索的 QBF 求解
DOI：
--
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Florian Lonsing
中科院分区：
文献类型：
--
作者：
Florian Lonsing
DepQBF是一个基于搜索的量化布尔公式(QBF)求解器，实现了QCDCL范式。我们将DepQBF作为几个工具包的一部分提交给QBFEVAL‘18比赛，这是2018年Floc奥运会的一部分。这些包集成了DepQBF作为后端QBF解算器和称为QBFRelay的预处理前端。该前端由一个外壳脚本组成，该脚本在给定的QBF上的多个轮次中运行多个预处理器，从而导致增量预处理。QBFRelay使用由QBF社区开发的公开可用的预处理器，此外，我们的新型预处理器QRATPre+是基于QRAT证明系统的推广。我们介绍了DepQBF、QRATPre+和QBFRelay的概况，并报告了我们在Floc奥运会上获得奖牌的提交材料的表现。
DepQBF is a search-based quantified Boolean formula (QBF) solver implementing the QCDCL paradigm. We submitted DepQBF as part of several tool packages to the QBFEVAL’18 competition, which was part of the FLoC Olympic Games 2018. These packages integrate DepQBF as a back end QBF solver and a preprocessing front end called QBFRelay. This front end consists of a shell script that runs several preprocessors in multiple rounds on a given QBF, thus resulting in incremental preprocessing. QBFRelay employs publicly available preprocessors developed by the QBF community and, additionally, our novel preprocessor QRATPre+ that is based on a generalization of the QRAT proof system. We present an overview of DepQBF, QRATPre+, and QBFRelay and report on the performance of our submissions, which were awarded a medal in the FLoC Olympic Games.
DOI：
10.1007/s10817-008-9114-5
发表时间：
2009-01-01
期刊：
JOURNAL OF AUTOMATED REASONING
影响因子：
--
作者：
Samer, Marko;Szeider, Stefan
通讯作者：
Szeider, Stefan