Breaking Symmetries in Quantified Graph Search: A Comparative Study

TL;DR

This paper extends the SAT Modulo Symmetries framework to handle quantified Boolean formulas, enabling more expressive graph symmetry breaking with two approaches, balancing speed and implementation ease.

Contribution

It introduces novel methods to incorporate symmetry breaking into QBF solving, expanding the applicability beyond propositional logic.

Findings

QBF-based symmetry breaking is easier to implement and verify.

Specialized methods can be faster for certain problems.

The extended framework handles complex constraints like non-3-colorability.

Abstract

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.