QRATPre+: Effective QBF Preprocessing via Strong Redundancy Properties
Logic in Computer Science
2019-07-03 v2
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.
Cite
@article{arxiv.1904.12927,
title = {QRATPre+: Effective QBF Preprocessing via Strong Redundancy Properties},
author = {Florian Lonsing and Uwe Egly},
journal= {arXiv preprint arXiv:1904.12927},
year = {2019}
}
Comments
preprint of a paper to be published at SAT 2019, LNCS, Springer, including appendix