Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2410.15848 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912555672272896 |
|---|---|
| author | Hofstadler, Clemens Kauers, Manuel Seidl, Martina |
| author_facet | Hofstadler, Clemens Kauers, Manuel Seidl, Martina |
| contents | Symmetries have been exploited successfully within the realms of SAT and QBF to improve solver performance in practical applications and to devise more powerful proof systems. As a first step towards extending these advancements to the class of dependency quantified Boolean formulas (DQBFs), which generalize QBF by allowing more nuanced variable dependencies, this work develops a comprehensive theory to characterize symmetries for DQBFs. We also introduce the notion of symmetry breakers of DQBFs, along with a concrete construction, and discuss how to detect DQBF symmetries algorithmically using a graph-based approach. Moreover, we empirically study the presence of symmetries in benchmark formulas and their impact on solving times. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2410_15848 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Symmetries of Dependency Quantified Boolean Formulas Hofstadler, Clemens Kauers, Manuel Seidl, Martina Logic in Computer Science Symmetries have been exploited successfully within the realms of SAT and QBF to improve solver performance in practical applications and to devise more powerful proof systems. As a first step towards extending these advancements to the class of dependency quantified Boolean formulas (DQBFs), which generalize QBF by allowing more nuanced variable dependencies, this work develops a comprehensive theory to characterize symmetries for DQBFs. We also introduce the notion of symmetry breakers of DQBFs, along with a concrete construction, and discuss how to detect DQBF symmetries algorithmically using a graph-based approach. Moreover, we empirically study the presence of symmetries in benchmark formulas and their impact on solving times. |
| title | Symmetries of Dependency Quantified Boolean Formulas |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2410.15848 |