ECCC-Report TR19-057https://eccc.weizmann.ac.il/report/2019/057Comments and Revisions published for TR19-057en-usSun, 14 Apr 2019 13:26:19 +0300
Paper TR19-057
| Proof Complexity of Symmetry Learning in QBF |
Joshua Blinkhorn,
Olaf Beyersdorff
https://eccc.weizmann.ac.il/report/2019/057For 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.Sun, 14 Apr 2019 13:26:19 +0300https://eccc.weizmann.ac.il/report/2019/057