Breaking Symmetries in Quantified Graph Search: A Comparative Study
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866909503437406208 |
|---|---|
| author | Janota, Mikoláš Kirchweger, Markus Peitl, Tomáš Szeider, Stefan |
| author_facet | Janota, Mikoláš Kirchweger, Markus Peitl, Tomáš Szeider, Stefan |
| contents | Graph generation and enumeration problems often require handling equivalent graphs -- those that differ only in vertex labeling. We study how to extend SAT Modulo Symmetries (SMS), a framework for eliminating such redundant graphs, to handle more complex constraints. While SMS was originally designed for constraints in propositional logic (in NP), we now extend it to handle quantified Boolean formulas (QBF), allowing for more expressive specifications like non-3-colorability (a coNP-complete property). We develop two approaches: a static QBF encoding and a dynamic method integrating SMS into QBF solvers. Our analysis reveals that while specialized approaches can be faster, QBF-based methods offer easier implementation and formal verification capabilities. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2502_15078 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Breaking Symmetries in Quantified Graph Search: A Comparative Study Janota, Mikoláš Kirchweger, Markus Peitl, Tomáš Szeider, Stefan Logic in Computer Science Graph generation and enumeration problems often require handling equivalent graphs -- those that differ only in vertex labeling. We study how to extend SAT Modulo Symmetries (SMS), a framework for eliminating such redundant graphs, to handle more complex constraints. While SMS was originally designed for constraints in propositional logic (in NP), we now extend it to handle quantified Boolean formulas (QBF), allowing for more expressive specifications like non-3-colorability (a coNP-complete property). We develop two approaches: a static QBF encoding and a dynamic method integrating SMS into QBF solvers. Our analysis reveals that while specialized approaches can be faster, QBF-based methods offer easier implementation and formal verification capabilities. |
| title | Breaking Symmetries in Quantified Graph Search: A Comparative Study |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2502.15078 |