2025/06/14 by Abdallah Saffidine, Saffidine, Abdallah, Andreas Herzig +1
Mathematics · Computer Science · #Approximation Theory and Sequence Spaces #Mathematical functions and polynomials #Optimization and Variational Analysis
paper · pdf · doi:10.48550/arxiv.2506.12562
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.