Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



TR19-057 | 6th April 2019 20:41

Proof Complexity of Symmetry Learning in QBF


Authors: Olaf Beyersdorff, Joshua Blinkhorn
Publication: 14th April 2019 13:26
Downloads: 625


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.

ISSN 1433-8092 | Imprint