Symmetries of Dependency Quantified Boolean Formulas

TL;DR

This paper develops a comprehensive theory of symmetries for dependency quantified Boolean formulas (DQBFs), introduces symmetry breakers, and empirically studies their impact on solver performance.

Contribution

It extends symmetry concepts from SAT and QBF to DQBFs, providing theoretical foundations, symmetry detection methods, and practical insights.

Findings

Symmetries are prevalent in DQBF benchmarks.

Symmetry breakers can improve solver efficiency.

Algorithmic detection of DQBF symmetries is feasible.

Abstract

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.