You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

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.