Symmetries of Quantified Boolean Formulas

TL;DR

This paper introduces a comprehensive framework for understanding and exploiting symmetries in quantified Boolean formulas (QBF), extending symmetry breaking techniques beyond existing limited approaches.

Contribution

It provides a general, unified characterization of QBF symmetries, including dualities, enabling more effective symmetry breaking in QBF solving.

Findings

Framework unifies symmetry concepts in QBF

Incorporates duality of universal and existential symmetries

Lays foundation for advanced symmetry breaking methods

Abstract

While symmetries are well understood for Boolean formulas and successfully exploited in practical SAT solving, less is known about symmetries in quantified Boolean formulas (QBF). There are some works introducing adaptions of propositional symmetry breaking techniques, with a theory covering only very specific parts of QBF symmetries. We present a general framework that gives a concise characterization of symmetries of QBF. Our framework naturally incorporates the duality of universal and existential symmetries resulting in a general basis for QBF symmetry breaking.