Polynomial Prenexing of QBFs with Non-Monotone Boolean Operators

TL;DR

This paper introduces a polynomial-time transformation for QBFs with non-monotone Boolean operators, extending prenexing techniques beyond traditional operators while preserving quantifier depth.

Contribution

It presents the first polynomial transformation for QBFs containing operators like biconditionals and XOR, expanding the scope of prenexing methods.

Findings

Transformation is polynomial in size.

Quantifier depth is preserved.

Applicable to a broader class of Boolean operators.

Abstract

It is well-known that every quantified boolean formula (QBF) can be transformed into a prenex QBF whose only boolean operators are negation, conjunction, and disjunction. It is also well-known that the transformation is polynomial if the boolean operators of the original QBF are restricted to negation, conjunction, and disjunction. In contrast, up to now no polynomial transformation has been found when the original QBF contains other boolean operators such as biconditionals or exclusive disjunction. We define such a transformation and show that it is polynomial and preserves quantifier depth.