18w5208 - Theory and Practice of Satisfiability Solving
Sprache des Tagungstitel:
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.