Polynomial Prenexing of QBFs with Non-Monotone Boolean Operators
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915343716319232 |
|---|---|
| author | Saffidine, Abdallah Herzig, Andreas |
| author_facet | Saffidine, Abdallah Herzig, Andreas |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2506_12562 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Polynomial Prenexing of QBFs with Non-Monotone Boolean Operators Saffidine, Abdallah Herzig, Andreas Computational Complexity 68Q15, 68Q17, 06E30 F.1.3; I.2.4; F.2.2 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. |
| title | Polynomial Prenexing of QBFs with Non-Monotone Boolean Operators |
| topic | Computational Complexity 68Q15, 68Q17, 06E30 F.1.3; I.2.4; F.2.2 |
| url | https://arxiv.org/abs/2506.12562 |