QRATPre+: Effective QBF Preprocessing via Strong Redundancy Properties
arXiv:1904.12927 · doi:10.1007/978-3-030-24258-9_14
Abstract
We present version 2.0 of QRATPre+, a preprocessor for quantified Boolean formulas (QBFs) based on the QRAT proof system and its generalization QRAT+. These systems rely on strong redundancy properties of clauses and universal literals. QRATPre+ is the first implementation of these redundancy properties in QRAT and QRAT+ used to simplify QBFs in preprocessing. It is written in C and features an API for easy integration in other QBF tools. We present implementation details and report on experimental results demonstrating that QRATPre+ improves upon the power of state-of-the-art preprocessors and solvers.
preprint of a paper to be published at SAT 2019, LNCS, Springer, including appendix