# QRATPre+: Effective QBF Preprocessing via Strong Redundancy Properties

arXiv: https://arxiv.org/abs/1904.12927 · HTML: https://mlsanity.com/paper/1904.12927/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 29 Apr 2019.

## Built on by (most cited first, 2 of 2)

- [Planning with Incomplete Information in Quantified Answer Set Programming](https://mlsanity.com/paper/2108.06405/) (2021)
- [Implicit State and Goals in QBF Encodings for Positional Games (extended version)](https://mlsanity.com/paper/2301.07345/) (2023)

## Abstract (arXiv)

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.