QBFRelay, QRATPre+, and DepQBF: Incremental Preprocessing Meets Search-Based QBF Solving

摘要

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.