For quantified Boolean formulas (QBF), a resolution system with a symmetry rule was recently introduced by Kauers and Seidl (Inf. Process. Lett. 2018). In this system, many formulas hard for QBF resolution admit short proofs.

Kauers and Seidl apply the symmetry rule on symmetries of the original formula. Here we propose a new formalism where symmetries are dynamically recomputed during the proof on restrictions of the original QBF. This presents a theoretical model for the potential use of symmetry learning as an inprocessing rule in QCDCL solving.

We demonstrate the power of symmetry learning by proving an exponential separation between Q-resolution with the symmetry rule and Q-resolution with our new symmetry learning rule. In fact, we show that bounding the number of symmetry recomputations gives rise to a hierarchy of QBF resolution systems of strictly increasing strength.