HQSpre - An Effective Preprocessor for QBF and DQBF. We present our new preprocessor HQSpre, a state-of-the-art tool for simplifying quantified Boolean formulas (QBFs) and the first available preprocessor for dependency quantified Boolean formulas (DQBFs). The latter are a generalization of QBFs, resulting from adding so-called Henkin-quantifiers to QBFs. HQSpre applies most of the preprocessing techniques that have been proposed in the literature. It can be used both as a standalone tool and as a library. It is possible to tailor it towards different solver back-ends, e. g., to preserve the circuit structure of the formula when a non-CNF solver back-end is used. Extensive experiments show that HQSpre allows QBF solvers to solve more benchmark instances and is able to decide more instances on its own than state-of-the-art tools. The same impact can be observed in the DQBF domain as well.
References in zbMATH (referenced in 2 articles )
Showing results 1 to 2 of 2.
- Pulina, Luca; Seidl, Martina: The 2016 and 2017 QBF solvers evaluations (QBFEVAL’16 and QBFEVAL’17) (2019)
- Lonsing, Florian; Egly, Uwe: (\textsfQRAT^+): generalizing QRAT by a more powerful QBF redundancy property (2018)