Short Proofs for Some Symmetric Quantified Boolean Formulas

TL;DR

This paper leverages symmetries to develop concise proofs for specific families of quantified Boolean formulas, enhancing proof complexity understanding and demonstrating separations among QBF proof systems.

Contribution

It introduces symmetry-based proof techniques and extends the Q-Res calculus with a symmetry rule, providing new insights into QBF proof complexity.

Findings

Short proofs for symmetric QBF families using symmetry breakers

Extension of Q-Res calculus with symmetry rule shows proof separations

Demonstrates the effectiveness of symmetry in simplifying QBF proofs

Abstract

We exploit symmetries to give short proofs for two prominent formula families of QBF proof complexity. On the one hand, we employ symmetry breakers. On the other hand, we enrich the (relatively weak) QBF resolution calculus Q-Res with the symmetry rule and obtain separations to powerful QBF calculi.