BIRS Workshop Lecture Videos
The Symmetry Rule for Quantified Boolean Formulas Seidl, Martina
One of the oldest and weakest calculi for quantified Boolean formulas
(QBF) is Q-Resolution. It consists of two rules: the resolution rule
similar as in propositional logic and the universal reduction rule. In
its most basic variant, resolution is allowed only over existential
variables. More powerful proof systems can be obtained by allowing
resolution over the universal variables as well or by introducing
so-called long-distance resolution. Separations are shown by using
the well-investigated formulas introduced by Kleine Buening and other
(the so-called KBKF formulas).
In this talk, we enrich the (relatively weak) QBF resolution calculus with the Symmetry Rule that exploits symmetries of the input formula. With this simple rule, we obtain separations to powerful QBF calculi by showing that the KBKF formulas and extensions become easy when the symmetry rule may be used.
Item Citations and Data
Attribution-NonCommercial-NoDerivatives 4.0 International