Breaking Symmetries in Quantified Graph Search: A Comparative Study

TL;DR

This work extends SAT Modulo Symmetries (SMS) to quantified graph search by integrating symmetry breaking into Quantified Boolean Formulas ($\mathrm{QBF}$). It introduces two main strategies: a static method (Q-static) that encodes canonicity with universal variables, and a dynamic method (Q-SMS) that embeds SMS within QBF solvers, complemented by a bespoke 2-QBF solver (2Qiss) and a co-certificate learning framework (CCL). Through benchmark classes such as triangle-free coloring, Folkman graphs, domination in cubic graphs, treewidth, snarks, and Kochen-Specker graphs, the study shows that Q-SMS offers a favorable balance of performance, verifiable proofs, and expressiveness, while Q-static scales poorly and CCL excels in some cases but lacks provable certificates. The results highlight the practicality of quantified graph search with SMS-enabled QBF solvers for producing independently verifiable results and point to future work on generalizing 2Qiss to arbitrary QBFs. The work thus contributes a robust, proof-enabled framework for exploiting symmetries in quantified graph problems with broad applicability in graph theory and beyond.

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.

Figures (1)

• Figure 1: CCL. CEGAR-based QBF solving with an SMS blackbox follows a similar pattern.

Theorems & Definitions (1)

• Conjecture 1