# QRATPre+: Effective QBF Preprocessing via Strong Redundancy Properties

## TL;DR

QRATPre+ is a new QBF preprocessor that uses advanced redundancy properties to simplify formulas, improving the effectiveness of QBF solving tools.

## Contribution

It introduces the first implementation of QRAT and QRAT+ redundancy properties in a preprocessor, enhancing QBF preprocessing capabilities.

## Key findings

- QRATPre+ outperforms existing preprocessors in experiments.
- It effectively reduces QBF formula complexity.
- The tool integrates easily with other QBF solvers.

## 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.